# HG changeset patch
# User wenzelm
# Date 1449929826 -3600
# Node ID 2111b95e692f1f58f9a907d4c275d13fbb058c09
# Parent  2154e6c8d52dd33f434fff106da67c387b0d9eea
tuned;

diff -r 2154e6c8d52d -r 2111b95e692f src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Fri Dec 11 13:44:20 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML	Sat Dec 12 15:17:06 2015 +0100
@@ -76,14 +76,13 @@
 type match_args = {multi : bool, cut : int};
 
 val parse_match_args =
-  Scan.optional (Args.parens (Parse.enum1 ","
-    (Args.$$$ "multi" -- Scan.succeed ~1 || Args.$$$ "cut" -- Scan.optional Parse.nat 1))) [] >>
-    (fn ss =>
-      fold (fn s => fn {multi, cut} =>
-        (case s of
-          ("multi", _) => {multi = true, cut = cut}
-        | ("cut", n) => {multi = multi, cut = n}))
-      ss {multi = false, cut = ~1});
+  Scan.optional
+    (Args.parens
+      (Parse.enum1 ","
+        (Args.$$$ "multi" >> (fn _ => fn {cut, ...} => {multi = true, cut = cut}) ||
+         Args.$$$ "cut" |-- Scan.optional Parse.nat 1
+          >> (fn n => fn {multi, ...} => {multi = multi, cut = n})))) []
+  >> (fn fs => fold I fs {multi = false, cut = ~1});
 
 fun parse_named_pats match_kind =
   Args.context --