src/Pure/Syntax/syntax.ML
changeset 21962 279b129498b6
parent 21826 b90d927e0a4b
child 22121 1950ae4fe5e0
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Dec 30 12:41:59 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Dec 30 16:08:00 2006 +0100
     1.3 @@ -394,11 +394,12 @@
     1.4      fun show_pt pt =
     1.5        Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
     1.6    in
     1.7 -    conditional (length pts > ! ambiguity_level) (fn () =>
     1.8 +    if length pts > ! ambiguity_level then
     1.9        if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
    1.10        else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
    1.11            "produces " ^ string_of_int (length pts) ^ " parse trees.");
    1.12 -         List.app (warning o show_pt) pts));
    1.13 +         List.app (warning o show_pt) pts)
    1.14 +    else ();
    1.15      SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
    1.16    end;
    1.17