1.1 --- a/src/HOL/Library/reflection.ML	Mon Jul 25 11:21:44 2011 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Mon Jul 25 11:21:45 2011 +0200
     1.3 @@ -312,7 +312,8 @@
     1.4      val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
     1.5    in rtac th i THEN TRY (rtac TrueI i) end);  (* FIXME THEN_ALL_NEW !? *)
     1.6  
     1.7 -fun reflection_tac ctxt = gen_reflection_tac ctxt (Codegen.evaluation_conv ctxt);
     1.8 -  (*FIXME why Codegen.evaluation_conv?  very specific...*)
     1.9 +fun reflection_tac ctxt = gen_reflection_tac ctxt
    1.10 +  (Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt));
    1.11 +  (*FIXME why Code_Evaluation.dynamic_conv?  very specific...*)
    1.12  
    1.13  end