# HG changeset patch
# User clasohm
# Date 793023911 -3600
# Node ID 77795af993153305d11219b7894bf81d45c476e5
# Parent  8e22076cd3caf7f2da1369db2b72f93f73820324
added check "length ts > 1" before printing ambiguity warning in infer_types

diff -r 8e22076cd3ca -r 77795af99315 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\