# HG changeset patch
# User Christian Sternagel
# Date 1374031154 -32400
# Node ID 72cda5eb5a391539f16d4d85fbd69c5631f154ee
# Parent  f4871fe80410d097d9fb9418878f49c598f56dfc
refactoring

diff -r f4871fe80410 -r 72cda5eb5a39 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Wed Jul 17 17:16:51 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML	Wed Jul 17 12:19:14 2013 +0900
@@ -137,9 +137,12 @@
     handle Type.TUNIFY => NONE
   end;
 
+fun get_instances ctxt (c, T) =
+  Same.function (get_variants ctxt) c
+  |> map_filter (unifiable_with (Proof_Context.theory_of ctxt) T);
+
 fun insert_variants_same ctxt t (Const (c, T)) =
-      (case map_filter (unifiable_with (Proof_Context.theory_of ctxt) T)
-         (Same.function (get_variants ctxt) c) of
+      (case get_instances ctxt (c, T) of
         [] => unresolved_overloading_error ctxt (c, T) t "no instances"
       | [variant] => variant
       | _ => raise Same.SAME)