src/Pure/ML/ml_lex.ML
changeset 43947 9b00f09f7721
parent 41502 967cbbc77abd
child 44706 fe319b45315c
     1.1 --- a/src/Pure/ML/ml_lex.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4  
     1.5  open Basic_Symbol_Pos;
     1.6  
     1.7 -fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg);
     1.8 +fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg);
     1.9  
    1.10  
    1.11  (* blanks *)