[isabelle-dev] Invoking Simplifier inside simproc, ### Simplifier: renamed bound variable

[Peter Lammich]

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