changeset 15032 | 02aed07e01bf |
parent 13875 | 12997e3ddd8d |
child 16417 | 9bc16273c2d4 |
--- a/src/HOL/Hoare/HoareAbort.thy Fri Jul 09 16:33:20 2004 +0200 +++ b/src/HOL/Hoare/HoareAbort.thy Sun Jul 11 20:33:22 2004 +0200 @@ -245,7 +245,7 @@ method_setup vcg_simp = {* Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => - hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *} + hoare_tac (asm_full_simp_tac (local_simpset_of ctxt))1)) *} "verification condition generator plus simplification" (* Special syntax for guarded statements and guarded array updates: *)