# HG changeset patch
# User Christian Sternagel
# Date 1376044463 -32400
# Node ID 83d9984ee6396c2d570d5687218ed94f0765d142
# Parent  47db379a6cf9c3289dcfcfead05e75f42ec3c6ba
avoid misleading "instances" in function name;

diff -r 47db379a6cf9 -r 83d9984ee639 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Fri Aug 09 19:34:23 2013 +0900
+++ b/src/Tools/adhoc_overloading.ML	Fri Aug 09 19:34:23 2013 +0900
@@ -142,13 +142,13 @@
     val maxidx2 = Term.maxidx_typ T2' maxidx1;
   in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end;
 
-fun get_instances ctxt (c, T) =
+fun get_candidates ctxt (c, T) =
   Same.function (get_variants ctxt) c
   |> 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
+      (case get_candidates ctxt (c, T) of
         [] => unresolved_overloading_error ctxt (c, T) t []
       | [variant] => variant
       | _ => raise Same.SAME)
@@ -182,7 +182,7 @@
     fun check_unresolved t =
       (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
         [] => ()
-      | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t (get_instances ctxt (c, T)));
+      | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t (get_candidates ctxt (c, T)));
     val _ = map check_unresolved ts;
   in NONE end;