# HG changeset patch
# User wenzelm
# Date 1427123432 -3600
# Node ID bc04a20e5a378f58038d82fcaa700870baa8bb4d
# Parent  00b62aa9f43011707542205e01e3c3b91138578e
tuned signature;

diff -r 00b62aa9f430 -r bc04a20e5a37 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Mon Mar 23 15:55:41 2015 +0100
+++ b/src/Pure/Isar/parse.ML	Mon Mar 23 16:10:32 2015 +0100
@@ -91,7 +91,6 @@
   val const_decl: (string * string * mixfix) parser
   val const_binding: (binding * string * mixfix) parser
   val params: (binding * string option) list parser
-  val simple_fixes: (binding * string option) list parser
   val fixes: (binding * string option * mixfix) list parser
   val for_fixes: (binding * string option * mixfix) list parser
   val ML_source: Input.source parser
@@ -360,8 +359,6 @@
 val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
   >> (fn (xs, T) => map (rpair T) xs);
 
-val simple_fixes = and_list1 params >> flat;
-
 val fixes =
   and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) ||
     params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
diff -r 00b62aa9f430 -r bc04a20e5a37 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Mon Mar 23 15:55:41 2015 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Mon Mar 23 16:10:32 2015 +0100
@@ -132,8 +132,9 @@
 val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
 
 val obtain_case =
-  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
-    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
+  Parse.parbinding --
+    (Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --
+      (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
 
 val general_statement =
   statement >> (fn x => ([], Element.Shows x)) ||