changeset 15032 | 02aed07e01bf |
parent 13857 | 11d7c5a8dbb7 |
child 16417 | 9bc16273c2d4 |
--- a/src/HOL/Hoare/Hoare.thy Fri Jul 09 16:33:20 2004 +0200 +++ b/src/HOL/Hoare/Hoare.thy Sun Jul 11 20:33:22 2004 +0200 @@ -235,7 +235,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" end