1.1 --- a/src/HOL/Library/reflection.ML	Thu Jul 23 18:44:08 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Thu Jul 23 18:44:09 2009 +0200
     1.3 @@ -285,7 +285,7 @@
     1.4      val th' = instantiate ([], cvs) th
     1.5      val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
     1.6      val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
     1.7 -	       (fn _ => simp_tac (local_simpset_of ctxt) 1)
     1.8 +	       (fn _ => simp_tac (simpset_of ctxt) 1)
     1.9    in FWD trans [th'',th']
    1.10    end
    1.11