| changeset 62969 | 9f394a16c557 |
| parent 62848 | e4140efe699e |
| child 63429 | baedd4724f08 |
--- a/src/Pure/Tools/find_consts.ML Wed Apr 13 17:00:02 2016 +0200 +++ b/src/Pure/Tools/find_consts.ML Wed Apr 13 18:01:05 2016 +0200 @@ -136,7 +136,7 @@ local val criterion = - Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || + Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.name) >> Name || Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict || Parse.typ >> Loose;