src/Pure/sign.ML
changeset 901 77795af99315
parent 881 d7dcba167ed8
child 922 196ca0973a6d
     1.1 --- a/src/Pure/sign.ML	Thu Feb 16 08:55:15 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Feb 17 13:25:11 1995 +0100
     1.3 @@ -292,7 +292,7 @@
     1.4        | process_terms [] (idx, infrd_t, tye) msg _ = 
     1.5            if msg = "" then (the idx, the infrd_t, the tye) 
     1.6            else
     1.7 -            (if length ts <= !Syntax.ambiguity_level then
     1.8 +            (if length ts > 1 andalso length ts <= !Syntax.ambiguity_level then
     1.9                                                        (*no warning shown yet?*)
    1.10                 writeln "Warning: Currently parsed input \
    1.11                         \produces more than one parse tree.\n\