src/Pure/sign.ML

--- a/src/Pure/sign.ML	Thu Jan 26 13:31:36 1995 +0100
+++ b/src/Pure/sign.ML	Fri Jan 27 12:28:05 1995 +0100
@@ -64,7 +64,6 @@
     val pure: sg
     val const_of_class: class -> string
     val class_of_const: string -> class
-    val ambiguity_level: int ref
   end
 end;
 
@@ -245,8 +244,6 @@
 
 (** infer_types **)         (*exception ERROR*)
 
-val ambiguity_level = ref 1;
-
 fun infer_types sg types sorts print_msg (ts, T) =
   let
     val Sg {tsig, ...} = sg;
@@ -294,10 +291,17 @@
          end
       | process_terms [] (idx, infrd_t, tye) msg _ = 
           if msg = "" then (the idx, the infrd_t, the tye) 
-          else error msg;
+          else
+            (if 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 ();
+             error msg)
 
     val (idx, infrd_t, tye) = process_terms ts (None, None, None) "" 0;
-  in if print_msg andalso length ts > !ambiguity_level then
+  in if print_msg andalso length ts > !Syntax.ambiguity_level then
        writeln "Fortunately, only one parse tree is type correct.\n\
          \It helps (speed!) if you disambiguate your grammar or your input."
      else ();