diff -r 9c25418db6f0 -r 5baaabe1ab92 CookBook/Parsing.thy --- 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