| changeset 44357 | 5f5649ac8235 |
| parent 42287 | d98eb048a2e4 |
| child 45592 | 8baa0b7f3f66 |
--- a/src/Pure/Isar/parse_spec.ML Sun Aug 21 20:25:49 2011 +0200 +++ b/src/Pure/Isar/parse_spec.ML Sun Aug 21 20:42:26 2011 +0200 @@ -136,7 +136,7 @@ val expr0 = plus1_unless locale_keyword expr1; in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; -val context_element = Parse.group "context element" loc_element; +val context_element = Parse.group (fn () => "context element") loc_element; end;