# HG changeset patch
# User wenzelm
# Date 1185712200 -7200
# Node ID 8c168f5ef22175b354bcb733bb4deda8ce4dfa34
# Parent  9b156986a4e983fe6a0e02ef792dfbcf04b128b7
avoid ill-defined Simp_tac;

diff -r 9b156986a4e9 -r 8c168f5ef221 src/HOL/ex/reflection.ML
--- a/src/HOL/ex/reflection.ML	Sun Jul 29 14:29:59 2007 +0200
+++ b/src/HOL/ex/reflection.ML	Sun Jul 29 14:30:00 2007 +0200
@@ -285,7 +285,7 @@
   val th' = instantiate ([], cvs) th
   val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
   val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
-			(fn _ => Simp_tac 1)
+			(fn _ => simp_tac (local_simpset_of ctxt) 1)
   val _ = bds := []
 in FWD trans [th'',th']
 end