| changeset 69580 | 6f755e3cd95d |
| parent 69579 | edea246cedb3 |
| child 69876 | b49bd228ac8a |
--- a/src/Pure/Isar/parse.ML Thu Jan 03 16:13:57 2019 +0100 +++ b/src/Pure/Isar/parse.ML Thu Jan 03 16:42:15 2019 +0100 @@ -328,7 +328,7 @@ local -val mfix = input string; +val mfix = input (string || cartouche); val mixfix_ = mfix -- !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000)