src/Pure/type_infer.ML
changeset 24485 687bbb686ef9
parent 24275 bbc3dab6d4fe
child 24504 0edc609e36fd
     1.1 --- a/src/Pure/type_infer.ML	Thu Aug 30 15:04:42 2007 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Thu Aug 30 15:04:44 2007 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val paramify_vars: typ -> typ
     1.5    val paramify_dummies: typ -> int -> typ * int
     1.6    val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
     1.7 -  val infer_types: Pretty.pp -> Type.tsig -> Type.mode ->
     1.8 +  val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
     1.9      (string -> typ option) -> (indexname -> typ option) ->
    1.10      Name.context -> bool -> (term * typ) list -> (term * typ) list * (indexname * typ) list
    1.11  end;
    1.12 @@ -381,13 +381,12 @@
    1.13  
    1.14  (* infer_types *)
    1.15  
    1.16 -fun infer_types pp tsig mode const_type var_type used freeze args =
    1.17 +fun infer_types pp tsig check_typs const_type var_type used freeze args =
    1.18    let
    1.19 -    (*certify types*)
    1.20 -    fun certT T = Type.cert_typ_mode mode tsig T;
    1.21 +    (*check types*)
    1.22      val (raw_ts, raw_Ts) = split_list args;
    1.23 -    val ts = map (Term.map_types certT) raw_ts;
    1.24 -    val Ts = map certT raw_Ts;
    1.25 +    val ts = burrow_types check_typs raw_ts;
    1.26 +    val Ts = check_typs raw_Ts;
    1.27  
    1.28      (*constrain vars*)
    1.29      val get_type = the_default dummyT o var_type;