| changeset 44357 | 5f5649ac8235 |
| parent 44160 | 8848867501fb |
| child 46737 | 09ab89658a5d |
--- a/src/Pure/Thy/thy_header.ML Sun Aug 21 20:25:49 2011 +0200 +++ b/src/Pure/Thy/thy_header.ML Sun Aug 21 20:42:26 2011 +0200 @@ -29,8 +29,8 @@ (* header args *) -val file_name = Parse.group "file name" Parse.name; -val theory_name = Parse.group "theory name" Parse.name; +val file_name = Parse.group (fn () => "file name") Parse.name; +val theory_name = Parse.group (fn () => "theory name") Parse.name; val file = Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||