src/Pure/Isar/parse_spec.ML

--- a/src/Pure/Isar/parse_spec.ML	Mon May 30 11:44:41 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Mon May 30 14:15:44 2016 +0200
@@ -60,7 +60,7 @@
 
 val multi_specs =
   Parse.enum1 "|"
-    (opt_thm_name ":" -- Parse.prop -- if_assumes --|
+    ((opt_thm_name ":" -- Parse.prop -- if_assumes -- Parse.for_fixes >> Scan.triple1) --|
       Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
 
 val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;