src/Pure/Syntax/syntax.ML

   val basic_nonterms: string list
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
   val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
-  val standard_parse_term: Pretty.pp -> (term -> term Exn.result) ->
+  val standard_parse_term: Pretty.pp -> (term -> string option) ->
     (((string * int) * sort) list -> string * int -> Term.sort) ->
     (string -> string option) -> (string -> string option) ->
     (typ -> typ) -> (sort -> sort) -> Proof.context ->
     (string -> bool) -> syntax -> typ -> string -> term
   val standard_parse_typ: Proof.context -> syntax ->

 
 (*brute-force disambiguation via type-inference*)
 fun disambig _ _ [t] = t
   | disambig pp check ts =
       let
-        val err_results = map check ts;
-        val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
-        val results = map_filter Exn.get_result err_results;
+        val errs = map check ts;
+        val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
 
         val ambiguity = length ts;
         fun ambig_msg () =
           if ambiguity > 1 andalso ambiguity <= ! ambiguity_level then
             "Got more than one parse tree.\n\
             \Retry with smaller ambiguity_level for more information."
           else "";
       in
-        if null results then cat_error (ambig_msg ()) (cat_lines errs)
+        if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
         else if length results = 1 then
           (if ambiguity > ! ambiguity_level then
             warning "Fortunately, only one parse tree is type correct.\n\
               \You may still want to disambiguate your grammar or your input."
           else (); hd results)