diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Library/Reflection.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -16,10 +16,10 @@
 
 use "reflection.ML"
 
-method_setup reify = {* fn src =>
-  Method.syntax (Attrib.thms --
-    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
-  (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
+method_setup reify = {*
+  Attrib.thms --
+    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
+  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
 *} "partial automatic reification"
 
 method_setup reflection = {* 
@@ -30,16 +30,17 @@
   val any_keyword = keyword onlyN || keyword rulesN;
   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   val terms = thms >> map (term_of o Drule.dest_term);
-  fun optional scan = Scan.optional scan [];
-in fn src =>
-  Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
-    (fn (((eqs,ths),to), ctxt) => 
-      let 
-        val (ceqs,cths) = Reify_Data.get ctxt 
-        val corr_thms = ths@cths
-        val raw_eqs = eqs@ceqs
-      in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
-     end) end
-*} "reflection method"
+in
+  thms --
+  Scan.optional (keyword rulesN |-- thms) [] --
+  Scan.option (keyword onlyN |-- Args.term) >>
+  (fn ((eqs,ths),to) => fn ctxt =>
+    let 
+      val (ceqs,cths) = Reify_Data.get ctxt 
+      val corr_thms = ths@cths
+      val raw_eqs = eqs@ceqs
+    in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
+end
+*} "reflection"
 
 end