src/HOL/Hoare/HoareAbort.thy

--- a/src/HOL/Hoare/HoareAbort.thy	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy	Thu Jul 23 18:44:09 2009 +0200
@@ -251,7 +251,7 @@
 
 method_setup vcg_simp = {*
   Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
+    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *}
   "verification condition generator plus simplification"
 
 (* Special syntax for guarded statements and guarded array updates: *)