tuned signature;
authorwenzelm
Mon Apr 18 20:40:31 2011 +0200 (2011-04-18)
changeset 42398919e17c0358e
parent 42397 13798dcbdca5
child 42399 95b17b4901b5
tuned signature;
src/Tools/subtyping.ML
     1.1 --- a/src/Tools/subtyping.ML	Mon Apr 18 17:07:47 2011 +0200
     1.2 +++ b/src/Tools/subtyping.ML	Mon Apr 18 20:40:31 2011 +0200
     1.3 @@ -6,13 +6,9 @@
     1.4  
     1.5  signature SUBTYPING =
     1.6  sig
     1.7 -  datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
     1.8    val coercion_enabled: bool Config.T
     1.9 -  val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
    1.10 -    term list -> term list
    1.11    val add_type_map: term -> Context.generic -> Context.generic
    1.12    val add_coercion: term -> Context.generic -> Context.generic
    1.13 -  val gen_coercion: Proof.context -> typ Vartab.table -> (typ * typ) -> term
    1.14    val setup: theory -> theory
    1.15  end;
    1.16  
    1.17 @@ -666,8 +662,11 @@
    1.18  
    1.19  (** assembling the pipeline **)
    1.20  
    1.21 -fun infer_types ctxt const_type var_type raw_ts =
    1.22 +fun coercion_infer_types ctxt raw_ts =
    1.23    let
    1.24 +    val const_type = try (Consts.the_constraint (Proof_Context.consts_of ctxt));
    1.25 +    val var_type = Proof_Context.def_type ctxt;
    1.26 +
    1.27      val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts;
    1.28  
    1.29      fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
    1.30 @@ -714,11 +713,6 @@
    1.31  
    1.32  (* term check *)
    1.33  
    1.34 -fun coercion_infer_types ctxt =
    1.35 -  infer_types ctxt
    1.36 -    (try (Consts.the_constraint (Proof_Context.consts_of ctxt)))
    1.37 -    (Proof_Context.def_type ctxt);
    1.38 -
    1.39  val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false);
    1.40  
    1.41  val add_term_check =