diff -r 716fec31f9ea -r 06b19a7e675a src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Aug 29 18:39:47 2003 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Aug 31 21:24:29 2003 +0200
@@ -61,11 +61,13 @@
   val simple_string_of_typ: typ -> string
   val simple_pprint_typ: typ -> pprint_args -> unit
   val ambiguity_level: int ref
+  val ambiguity_is_error: bool ref
 end;
 
 structure Syntax: SYNTAX =
 struct
 
+val ambiguity_is_error = ref false
 
 (** tables of translation functions **)
 
@@ -350,9 +352,12 @@
       warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
   in
     if length pts > ! ambiguity_level then
-      (warning ("Ambiguous input " ^ quote str);
-       warning "produces the following parse trees:";
-       seq show_pt pts)
+	if ! ambiguity_is_error then
+	    error ("Ambiguous input " ^ quote str)
+	else
+	    (warning ("Ambiguous input " ^ quote str);
+	     warning "produces the following parse trees:";
+	     seq show_pt pts)
     else ();
     map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts
   end;