# HG changeset patch
# User wenzelm
# Date 1320361665 -3600
# Node ID 6e0a8aba99ec4d96638f72ea91ed9ac8c40ef7bd
# Parent  93b8e30a5d1f1ae14e5198821933aa0da855ca43
more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax);

diff -r 93b8e30a5d1f -r 6e0a8aba99ec src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Thu Nov 03 23:55:53 2011 +0100
+++ b/src/Pure/Isar/parse.ML	Fri Nov 04 00:07:45 2011 +0100
@@ -322,7 +322,7 @@
 val simple_fixes = and_list1 params >> flat;
 
 val fixes =
-  and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
+  and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) ||
     params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
 
 val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];