On Mo, 2012-04-02 at 13:45 +0200, Makarius wrote: > On Mon, 26 Mar 2012, Peter Lammich wrote: > > > I tried to follow the approach done in the cancellation simprocs, > > getting something like: > > > > fun assn_simproc_fun ss credex = let > > val ctxt = Simplifier.the_context ss > > val ([redex],ctxt') = Variable.import_terms true [term_of credex] > > ctxt; > > val export = singleton (Variable.export ctxt' ctxt) > > > > fun do_transform t = [...] > > > > val new_form = do_transform redex; > > > > val result = Option.map (export o mk_meta_eq) > > (Arith_Data.prove_conv_nohyps > > [simp_tac (HOL_basic_ss addsimps @{thms star_aci}) 1] ctxt > > (redex,new_form) > > ); > > > > in result > > end; > > > > Where do_transform does the job of transforming the term. > > However, I get strange warning messages starting with > > "### Simplifier: renamed bound variable ...", I guess from the inner > > call to the simplifier. When tracing the value of "redex", I find that > > it may contain loose bound variables, and the warnings from the > > simplifier seem to be related to "redex" containing loose bound vars. > > > > Now my question: Are these "renamed bound variable" - messages from the > > simplifier harmful? What am I doing wrong, and how to do it properly? > > The warning is annoying, but not immediately harmful -- we have lived with > such issues of "non-localized" simprocs for many years in main HOL, until > Brian managed to isolate the last one 1-2 years ago. > > I reckon that you merely need to use (Simplifier.context ctxt) or > (Simplifier.inherit_context ss) on the nested simpset above to get rid of > the warning.
Thank you. Using the simpset "Simplifier.inherit_context ss (HOL_basic_ss addsimps @{thms star_aci})" did the job! Cheers, Peter _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev