src/Pure/sign.ML
changeset 24370 757b093e3459
parent 24273 1d4b411caf44
child 24485 687bbb686ef9
     1.1 --- a/src/Pure/sign.ML	Mon Aug 20 23:41:35 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Aug 20 23:41:37 2007 +0200
     1.3 @@ -568,40 +568,14 @@
     1.4    let
     1.5      val thy = ProofContext.theory_of ctxt;
     1.6  
     1.7 -    fun infer args = TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
     1.8 +    fun infer args = TypeInfer.infer_types pp (tsig_of thy)
     1.9          Type.mode_default (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst
    1.10        handle TYPE (msg, _, _) => error msg;
    1.11  
    1.12 -    (*brute-force disambiguation via type-inference*)
    1.13 -    fun disambig _ [t] = t
    1.14 -      | disambig T ts =
    1.15 -          let
    1.16 -            fun try_infer t = Exn.Result (singleton (fst o infer) (t, T))
    1.17 -              handle ERROR msg => Exn.Exn (ERROR msg);
    1.18 -            val err_results = map try_infer ts;
    1.19 -            val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
    1.20 -            val results = map_filter Exn.get_result err_results;
    1.21 -
    1.22 -            val ambiguity = length ts;
    1.23 -            fun ambig_msg () =
    1.24 -              if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level then
    1.25 -                "Got more than one parse tree.\n\
    1.26 -                \Retry with smaller Syntax.ambiguity_level for more information."
    1.27 -              else "";
    1.28 -          in
    1.29 -            if null results then cat_error (ambig_msg ()) (cat_lines errs)
    1.30 -            else if length results = 1 then
    1.31 -              (if ambiguity > ! Syntax.ambiguity_level then
    1.32 -                warning "Fortunately, only one parse tree is type correct.\n\
    1.33 -                  \You may still want to disambiguate your grammar or your input."
    1.34 -              else (); hd results)
    1.35 -            else cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^
    1.36 -              cat_lines (map (Pretty.string_of_term pp) ts))
    1.37 -          end;
    1.38 -
    1.39 -    (*read term*)
    1.40 +    fun check T t = Exn.Result (singleton (fst o infer) (t, T))
    1.41 +      handle ERROR msg => Exn.Exn (ERROR msg);
    1.42      val map_const = try (#1 o Term.dest_Const o Consts.read_const consts);
    1.43 -    fun read T = disambig T o Syntax.standard_parse_term (get_sort thy def_sort) map_const map_free
    1.44 +    fun read T = Syntax.standard_parse_term pp (check T) (get_sort thy def_sort) map_const map_free
    1.45          (intern_tycons thy) (intern_sort thy) ctxt is_logtype syn T;
    1.46    in
    1.47      raw_args