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