# HG changeset patch
# User Christian Sternagel
# Date 1376044463 -32400
# Node ID 38165b99562ea985431641aa5051604cc0ac5fc4
# Parent  39da27fc6101dc0509a24378bc3ebd312ced81b1
clarify function;

diff -r 39da27fc6101 -r 38165b99562e src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Tue Aug 13 13:18:26 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML	Fri Aug 09 19:34:23 2013 +0900
@@ -135,19 +135,17 @@
 
 (* check / uncheck *)
 
-fun unifiable_with thy T1 (t, T2) =
+fun unifiable_with thy T1 T2 =
   let
     val maxidx1 = Term.maxidx_of_typ T1;
     val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
     val maxidx2 = Term.maxidx_typ T2' maxidx1;
-  in
-    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME t)
-    handle Type.TUNIFY => NONE
-  end;
+  in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end;
 
 fun get_instances ctxt (c, T) =
   Same.function (get_variants ctxt) c
-  |> map_filter (unifiable_with (Proof_Context.theory_of ctxt) T);
+  |> map_filter (fn (t, T') =>
+    if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t else NONE);
 
 fun insert_variants_same ctxt t (Const (c, T)) =
       (case get_instances ctxt (c, T) of