avoid misleading "instances" in function name;
authorChristian Sternagel
Fri, 09 Aug 2013 19:34:23 +0900
changeset 53006 83d9984ee639
parent 53005 47db379a6cf9
child 53007 54e290da6da8
avoid misleading "instances" in function name;
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;