replacing conversion function of old code generator by the current code generator in the reflection tactic
authorbulwahn
Mon, 25 Jul 2011 11:21:45 +0200
changeset 43960 c2554cc82d34
parent 43959 285ffb18da30
child 43961 91294d386539
replacing conversion function of old code generator by the current code generator in the reflection tactic
src/HOL/Library/reflection.ML
--- 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