# HG changeset patch
# User bulwahn
# Date 1311585705 -7200
# Node ID c2554cc82d34a9515e2d2ed749c6feef6bca0c77
# Parent  285ffb18da304977cdb0feaadff91083b1132b90
replacing conversion function of old code generator by the current code generator in the reflection tactic

diff -r 285ffb18da30 -r c2554cc82d34 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