# HG changeset patch # User wenzelm # Date 921185723 -3600 # Node ID f05492a711b1f93545090f7d4b6d462c39614d15 # Parent a4c75cbd2fbfcd0577dea06ac45cb0013fa1b22e tuned opt_mixfix failure; diff -r a4c75cbd2fbf -r f05492a711b1 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Thu Mar 11 21:53:50 1999 +0100 +++ b/src/Pure/Isar/outer_parse.ML Thu Mar 11 21:55:23 1999 +0100 @@ -188,7 +188,7 @@ Scan.optional ($$$ "(" |-- !!! (fix --| $$$ ")")) Syntax.NoSyn; val opt_infix = opt_fix (infxl || infxr); -val opt_mixfix = opt_fix (mixfix || infxl || infxr || binder); +val opt_mixfix = opt_fix (mixfix || binder || infxl || infxr); (* consts *)