src/HOL/Hoare/Hoare.thy

 
 lemmas AbortRule = SkipRule  -- "dummy version"
 use "hoare_tac.ML"
 
 method_setup vcg = {*
-  Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
   "verification condition generator"
 
 method_setup vcg_simp = {*
-  Method.ctxt_args (fn ctxt =>
+  Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   "verification condition generator plus simplification"
 
 end