author | clasohm |
Fri, 17 Feb 1995 13:25:11 +0100 | |
changeset 901 | 77795af99315 |
parent 900 | 8e22076cd3ca |
child 902 | cc80f53b28c6 |
src/Pure/sign.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/sign.ML Thu Feb 16 08:55:15 1995 +0100 +++ b/src/Pure/sign.ML Fri Feb 17 13:25:11 1995 +0100 @@ -292,7 +292,7 @@ | process_terms [] (idx, infrd_t, tye) msg _ = if msg = "" then (the idx, the infrd_t, the tye) else - (if length ts <= !Syntax.ambiguity_level then + (if length ts > 1 andalso length ts <= !Syntax.ambiguity_level then (*no warning shown yet?*) writeln "Warning: Currently parsed input \ \produces more than one parse tree.\n\