src/Pure/type_infer.ML
changeset 24275 bbc3dab6d4fe
parent 22771 ce1fe6ca7dbb
child 24485 687bbb686ef9
     1.1 --- a/src/Pure/type_infer.ML	Tue Aug 14 23:22:58 2007 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Aug 14 23:23:00 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 ->
     1.8 +  val infer_types: Pretty.pp -> Type.tsig -> Type.mode ->
     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,10 +381,10 @@
    1.13  
    1.14  (* infer_types *)
    1.15  
    1.16 -fun infer_types pp tsig const_type var_type used freeze args =
    1.17 +fun infer_types pp tsig mode const_type var_type used freeze args =
    1.18    let
    1.19      (*certify types*)
    1.20 -    val certT = Type.cert_typ tsig;
    1.21 +    fun certT T = Type.cert_typ_mode mode tsig T;
    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;