Hi all, Referring to Isabelle-2011-1 (If this post belongs to the users list, feel free to answer it there)
I want to write a simplification procedure, that gets in a term t, does some transformations on it to obtain a term t', then invokes the simplifier (with some customized simpset) to prove "t=t'" and returns it as simplification lemma. 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? Best and thanks in advance for any help, Peter _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev