added check "length ts > 1" before printing ambiguity warning in infer_types
authorclasohm
Fri, 17 Feb 1995 13:25:11 +0100
changeset 901 77795af99315
parent 900 8e22076cd3ca
child 902 cc80f53b28c6
added check "length ts > 1" before printing ambiguity warning in infer_types
src/Pure/sign.ML
--- 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\