--- 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;