avoid multiple reports on shared type;
authorwenzelm
Mon, 06 Jun 2016 08:13:07 +0200
changeset 63230 ae5275fa96dc
parent 63229 f951c624c1a1
child 63231 54197a7c1bbd
avoid multiple reports on shared type;
src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sat Jun 04 16:54:23 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Mon Jun 06 08:13:07 2016 +0200
@@ -368,9 +368,11 @@
 val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> Scan.triple1;
 
 val param_mixfix = binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o Scan.triple1);
+
 val params =
-  Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
-    >> (fn (xs, T) => map (fn x => (x, T, NoSyn)) xs);
+  (binding -- Scan.repeat binding) -- Scan.option ($$$ "::" |-- !!! (Scan.ahead typ -- embedded))
+    >> (fn ((x, ys), T) =>
+        (x, Option.map #1 T, NoSyn) :: map (fn y => (y, Option.map #2 T, NoSyn)) ys);
 
 val fixes = and_list1 (param_mixfix || params) >> flat;
 val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];