--- a/src/HOL/Hoare/HoareAbort.thy Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy Wed Nov 29 15:44:51 2006 +0100
@@ -238,14 +238,12 @@
use "hoareAbort.ML"
method_setup vcg = {*
- Method.no_args
- (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
+ Method.no_args (Method.SIMPLE_METHOD' (hoare_tac (K all_tac))) *}
"verification condition generator"
method_setup vcg_simp = {*
Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- hoare_tac (asm_full_simp_tac (local_simpset_of ctxt))1)) *}
+ Method.SIMPLE_METHOD' (hoare_tac (asm_full_simp_tac (local_simpset_of ctxt)))) *}
"verification condition generator plus simplification"
(* Special syntax for guarded statements and guarded array updates: *)