replacing conversion function of old code generator by the current code generator in the reflection tactic
--- a/src/HOL/Library/reflection.ML Mon Jul 25 11:21:44 2011 +0200
+++ b/src/HOL/Library/reflection.ML Mon Jul 25 11:21:45 2011 +0200
@@ -312,7 +312,8 @@
val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
in rtac th i THEN TRY (rtac TrueI i) end); (* FIXME THEN_ALL_NEW !? *)
-fun reflection_tac ctxt = gen_reflection_tac ctxt (Codegen.evaluation_conv ctxt);
- (*FIXME why Codegen.evaluation_conv? very specific...*)
+fun reflection_tac ctxt = gen_reflection_tac ctxt
+ (Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt));
+ (*FIXME why Code_Evaluation.dynamic_conv? very specific...*)
end