Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/sign.ML
changeset 901 77795af99315
parent 881 d7dcba167ed8
child 922 196ca0973a6d 
--- 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\
isabelle