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

[Makarius]

On Mon, 2 Apr 2012, 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 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)
>>      );

Another fine point: redex lives in ctxt' so you should normally pass that 
to tools operating on it.


 	Makarius