src/Pure/sign.ML

               process_terms ts (Some n, infrd_t', tye') msg'' (n+1)
          end
       | 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\
                        \For more information lower Syntax.ambiguity_level."
              else ();