tuned signature;

--- a/src/Tools/subtyping.ML	Mon Apr 18 17:07:47 2011 +0200
+++ b/src/Tools/subtyping.ML	Mon Apr 18 20:40:31 2011 +0200
@@ -6,13 +6,9 @@
 
 signature SUBTYPING =
 sig
-  datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
   val coercion_enabled: bool Config.T
-  val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
-    term list -> term list
   val add_type_map: term -> Context.generic -> Context.generic
   val add_coercion: term -> Context.generic -> Context.generic
-  val gen_coercion: Proof.context -> typ Vartab.table -> (typ * typ) -> term
   val setup: theory -> theory
 end;
 
@@ -666,8 +662,11 @@
 
 (** assembling the pipeline **)
 
-fun infer_types ctxt const_type var_type raw_ts =
+fun coercion_infer_types ctxt raw_ts =
   let
+    val const_type = try (Consts.the_constraint (Proof_Context.consts_of ctxt));
+    val var_type = Proof_Context.def_type ctxt;
+
     val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts;
 
     fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
@@ -714,11 +713,6 @@
 
 (* term check *)
 
-fun coercion_infer_types ctxt =
-  infer_types ctxt
-    (try (Consts.the_constraint (Proof_Context.consts_of ctxt)))
-    (Proof_Context.def_type ctxt);
-
 val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false);
 
 val add_term_check =