avoid ill-defined Simp_tac;

--- 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