author | haftmann |
Fri, 24 Apr 2009 08:24:52 +0200 | |
changeset 30969 | fd9c89419358 |
parent 30968 | 10fef94f40fc |
child 30970 | 3fe2e418a071 |
--- a/src/HOL/Library/reflection.ML Thu Apr 23 12:17:51 2009 +0200 +++ b/src/HOL/Library/reflection.ML Fri Apr 24 08:24:52 2009 +0200 @@ -314,5 +314,6 @@ in (rtac th i THEN TRY(rtac TrueI i)) st end); fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv; + (*FIXME why Codegen.evaluation_conv? very specific...*) end