CookBook/Parsing.thy
changeset 181 5baaabe1ab92
parent 178 fb8f22dd8ad0
child 183 8bb4eaa2ec92
--- a/CookBook/Parsing.thy	Tue Mar 17 01:56:29 2009 +0100
+++ b/CookBook/Parsing.thy	Tue Mar 17 11:47:01 2009 +0100
@@ -993,9 +993,9 @@
 *}
 
 method_setup %gray foobar_meth = 
- {* Method.no_args 
-      (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *}
-        "foobar method"
+ {* Scan.succeed
+      (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
+         "foobar method"
 
 text {*
   It defines the method @{text foobar_meth} which takes no arguments and