# HG changeset patch
# User wenzelm
# Date 1465193587 -7200
# Node ID ae5275fa96dcc578d6bb63c5d55ae2a217144793
# Parent  f951c624c1a1430ee0cd7778daa01b02d94395f2
avoid multiple reports on shared type;

diff -r f951c624c1a1 -r ae5275fa96dc 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) [];