diff -r e0358fac0541 -r c2ee97a963db src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Jul 24 19:44:33 2007 +0200
+++ b/src/Pure/sign.ML	Tue Jul 24 19:44:35 2007 +0200
@@ -609,13 +609,13 @@
     val termss = fold_rev (multiply o fst) args [[]];
     val typs = map snd args;
 
-    fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
+    fun infer ts = Exn.Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
         (try (Consts.the_constraint consts)) def_type used freeze (ts ~~ typs) |>> map fst)
-      handle TYPE (msg, _, _) => Exn (ERROR msg);
+      handle TYPE (msg, _, _) => Exn.Exn (ERROR msg);
 
     val err_results = map infer termss;
-    val errs = map_filter (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
-    val results = map_filter get_result err_results;
+    val errs = map_filter (fn Exn.Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
+    val results = map_filter Exn.get_result err_results;
 
     val ambiguity = length termss;
     fun ambig_msg () =