# 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