tries to solve goal via TrueI

--- a/src/HOL/ex/reflection.ML	Wed Jul 11 17:47:52 2007 +0200
+++ b/src/HOL/ex/reflection.ML	Wed Jul 11 18:25:30 2007 +0200
@@ -320,7 +320,7 @@
     val t = the_default P to;
     val th = genreflect ctxt conv corr_thms raw_eqs t
       RS ssubst;
-  in rtac th i st end);
+  in (rtac th i THEN TRY(rtac TrueI i)) st end);
 
-fun reflection_tac ctxt = gen_reflection_tac ctxt NBE.normalization_conv;
+fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv;
 end