diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -454,7 +454,7 @@
 use "~~/src/HOL/Hoare/hoare_tac.ML"
 
 method_setup hoare = {*
-  Method.ctxt_args (fn ctxt =>
+  Scan.succeed (fn ctxt =>
     (SIMPLE_METHOD'
        (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}
   "verification condition generator for Hoare logic"