# HG changeset patch
# User nipkow
# Date 1184171130 -7200
# Node ID e105381d4140942c2de78914300ebf1d9ba27747
# Parent  97e41d1683115ad0a50644e19b89eff38977b7b4
tries to solve goal via TrueI

diff -r 97e41d168311 -r e105381d4140 src/HOL/ex/reflection.ML
--- 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