infer_types: general check_typs instead of Type.cert_typ_mode;

--- a/src/Pure/sign.ML	Thu Aug 30 15:04:42 2007 +0200
+++ b/src/Pure/sign.ML	Thu Aug 30 15:04:44 2007 +0200
@@ -567,9 +567,10 @@
     pp is_logtype syn consts map_free ctxt (def_type, def_sort) used freeze raw_args =
   let
     val thy = ProofContext.theory_of ctxt;
+    val check_typs = Syntax.check_typs (Type.set_mode Type.mode_default ctxt);
 
-    fun infer args = TypeInfer.infer_types pp (tsig_of thy)
-        Type.mode_default (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst
+    fun infer args = TypeInfer.infer_types pp (tsig_of thy) check_typs
+        (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst
       handle TYPE (msg, _, _) => error msg;
 
     fun check T t = Exn.Result (singleton (fst o infer) (t, T))

--- a/src/Pure/type_infer.ML	Thu Aug 30 15:04:42 2007 +0200
+++ b/src/Pure/type_infer.ML	Thu Aug 30 15:04:44 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 -> Type.mode ->
+  val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
     (string -> typ option) -> (indexname -> typ option) ->
     Name.context -> bool -> (term * typ) list -> (term * typ) list * (indexname * typ) list
 end;
@@ -381,13 +381,12 @@
 
 (* infer_types *)
 
-fun infer_types pp tsig mode const_type var_type used freeze args =
+fun infer_types pp tsig check_typs const_type var_type used freeze args =
   let
-    (*certify types*)
-    fun certT T = Type.cert_typ_mode mode tsig T;
+    (*check types*)
     val (raw_ts, raw_Ts) = split_list args;
-    val ts = map (Term.map_types certT) raw_ts;
-    val Ts = map certT raw_Ts;
+    val ts = burrow_types check_typs raw_ts;
+    val Ts = check_typs raw_Ts;
 
     (*constrain vars*)
     val get_type = the_default dummyT o var_type;