src/Pure/Thy/thy_output.ML
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;