src/Pure/ML/ml_parse.ML
changeset 43947 9b00f09f7721
parent 30682 dcb233670c98
child 43948 8f5add916a99
     1.1 --- a/src/Pure/ML/ml_parse.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Pure/ML/ml_parse.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -20,13 +20,13 @@
     1.4      fun get_pos [] = " (past end-of-file!)"
     1.5        | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok);
     1.6  
     1.7 -    fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
     1.8 -      | err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
     1.9 +    fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks)
    1.10 +      | err (toks, SOME msg) = (fn () => "SML syntax error" ^ get_pos toks ^ ": " ^ msg ());
    1.11    in Scan.!! err scan end;
    1.12  
    1.13  fun bad_input x =
    1.14    (Scan.some (fn tok => (case ML_Lex.kind_of tok of ML_Lex.Error msg => SOME msg | _ => NONE)) :|--
    1.15 -    (fn msg => Scan.fail_with (K msg))) x;
    1.16 +    (fn msg => Scan.fail_with (K (fn () => msg)))) x;
    1.17  
    1.18  
    1.19  (** basic parsers **)