src/Pure/sign.ML
changeset 23963 c2ee97a963db
parent 23660 18765718cf62
child 24142 6f6b698b9def
     1.1 --- a/src/Pure/sign.ML	Tue Jul 24 19:44:33 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Jul 24 19:44:35 2007 +0200
     1.3 @@ -609,13 +609,13 @@
     1.4      val termss = fold_rev (multiply o fst) args [[]];
     1.5      val typs = map snd args;
     1.6  
     1.7 -    fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
     1.8 +    fun infer ts = Exn.Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
     1.9          (try (Consts.the_constraint consts)) def_type used freeze (ts ~~ typs) |>> map fst)
    1.10 -      handle TYPE (msg, _, _) => Exn (ERROR msg);
    1.11 +      handle TYPE (msg, _, _) => Exn.Exn (ERROR msg);
    1.12  
    1.13      val err_results = map infer termss;
    1.14 -    val errs = map_filter (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
    1.15 -    val results = map_filter get_result err_results;
    1.16 +    val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
    1.17 +    val results = map_filter Exn.get_result err_results;
    1.18  
    1.19      val ambiguity = length termss;
    1.20      fun ambig_msg () =