# HG changeset patch
# User wenzelm
# Date 1449930049 -3600
# Node ID 3c19a230835f4cd62957d596657ff9176e984c6f
# Parent  afdbf76a0ded3b3bfdbd30505cfb91389d27589a
tuned;

diff -r afdbf76a0ded -r 3c19a230835f src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Sat Dec 12 15:17:54 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML	Sat Dec 12 15:20:49 2015 +0100
@@ -770,24 +770,22 @@
           end)
   end;
 
-val match_parser =
-  parse_match_kind :-- (fn kind =>
-      Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
-    (fn (matches, bodies) => fn ctxt => fn using =>
-      Method.RUNTIME (fn st =>
-        let
-          fun exec (pats, fixes, text) goal =
-            let
-              val ctxt' =
-                fold Variable.declare_term fixes ctxt
-                |> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*)
-            in real_match using ctxt' fixes matches text pats goal end;
-        in Seq.flat (Seq.FIRST (map exec bodies) st) end));
-
 val _ =
   Theory.setup
     (Method.setup @{binding match}
-      (match_parser >> (fn m => fn ctxt => METHOD_CASES (m ctxt)))
+      (parse_match_kind :--
+        (fn kind => Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
+        (fn (matches, bodies) => fn ctxt =>
+          METHOD_CASES (fn using => Method.RUNTIME (fn st =>
+            let
+              fun exec (pats, fixes, text) goal =
+                let
+                  val ctxt' =
+                    fold Variable.declare_term fixes ctxt
+                    (*FIXME Is this a good idea? We really only care about the maxidx*)
+                    |> fold (fn (_, t) => Variable.declare_term t) pats;
+                in real_match using ctxt' fixes matches text pats goal end;
+            in Seq.flat (Seq.FIRST (map exec bodies) st) end))))
       "structural analysis/matching on goals");
 
 end;