| changeset 40800 | 330eb65c9469 |
| parent 39689 | 78b185bf7660 |
| child 40801 | 6cfacec435e6 |
--- a/src/Pure/Thy/thy_output.ML Sun Nov 28 20:36:45 2010 +0100 +++ b/src/Pure/Thy/thy_output.ML Sun Nov 28 21:07:28 2010 +0100 @@ -162,7 +162,8 @@ in val antiq = - Parse.!!! (Parse.position Parse.xname -- properties -- Args.parse --| Scan.ahead Parse.eof) + Parse.!!! + (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof) >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); end;