# HG changeset patch
# User wenzelm
# Date 1187126580 -7200
# Node ID bbc3dab6d4fe3fe2dcd2d3b6bb9c06cc05b6197c
# Parent  cb9236269af18836cf476e84452b3650f16117e1
infer_types: depend on Type.mode;

diff -r cb9236269af1 -r bbc3dab6d4fe src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Tue Aug 14 23:22:58 2007 +0200
+++ b/src/Pure/type_infer.ML	Tue Aug 14 23:23:00 2007 +0200
@@ -15,7 +15,7 @@
   val paramify_vars: typ -> typ
   val paramify_dummies: typ -> int -> typ * int
   val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
-  val infer_types: Pretty.pp -> Type.tsig ->
+  val infer_types: Pretty.pp -> Type.tsig -> Type.mode ->
     (string -> typ option) -> (indexname -> typ option) ->
     Name.context -> bool -> (term * typ) list -> (term * typ) list * (indexname * typ) list
 end;
@@ -381,10 +381,10 @@
 
 (* infer_types *)
 
-fun infer_types pp tsig const_type var_type used freeze args =
+fun infer_types pp tsig mode const_type var_type used freeze args =
   let
     (*certify types*)
-    val certT = Type.cert_typ tsig;
+    fun certT T = Type.cert_typ_mode mode tsig T;
     val (raw_ts, raw_Ts) = split_list args;
     val ts = map (Term.map_types certT) raw_ts;
     val Ts = map certT raw_Ts;