| changeset 43947 | 9b00f09f7721 |
| parent 43432 | 224006e5ac46 |
| child 44706 | fe319b45315c |
--- a/src/Pure/Syntax/lexicon.ML Sat Jul 23 16:12:12 2011 +0200 +++ b/src/Pure/Syntax/lexicon.ML Sat Jul 23 16:37:17 2011 +0200 @@ -114,7 +114,7 @@ open Basic_Symbol_Pos; -fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg); +fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg); val scan_id = Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::