src/HOL/Library/reflection.ML
changeset 30969 fd9c89419358
parent 30743 2c83f7eaf1a4
child 31386 8624b75a7784
     1.1 --- a/src/HOL/Library/reflection.ML	Thu Apr 23 12:17:51 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Fri Apr 24 08:24:52 2009 +0200
     1.3 @@ -314,5 +314,6 @@
     1.4    in (rtac th i THEN TRY(rtac TrueI i)) st end);
     1.5  
     1.6  fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv;
     1.7 +  (*FIXME why Codegen.evaluation_conv?  very specific...*)
     1.8  
     1.9  end