infer_types: general check_typs instead of Type.cert_typ_mode;
authorwenzelm
Thu Aug 30 15:04:44 2007 +0200 (2007-08-30)
changeset 24485687bbb686ef9
parent 24484 013b98b57b86
child 24486 1dbf377c2e9a
infer_types: general check_typs instead of Type.cert_typ_mode;
src/Pure/sign.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/sign.ML	Thu Aug 30 15:04:42 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Aug 30 15:04:44 2007 +0200
     1.3 @@ -567,9 +567,10 @@
     1.4      pp is_logtype syn consts map_free ctxt (def_type, def_sort) used freeze raw_args =
     1.5    let
     1.6      val thy = ProofContext.theory_of ctxt;
     1.7 +    val check_typs = Syntax.check_typs (Type.set_mode Type.mode_default ctxt);
     1.8  
     1.9 -    fun infer args = TypeInfer.infer_types pp (tsig_of thy)
    1.10 -        Type.mode_default (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst
    1.11 +    fun infer args = TypeInfer.infer_types pp (tsig_of thy) check_typs
    1.12 +        (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst
    1.13        handle TYPE (msg, _, _) => error msg;
    1.14  
    1.15      fun check T t = Exn.Result (singleton (fst o infer) (t, T))
     2.1 --- a/src/Pure/type_infer.ML	Thu Aug 30 15:04:42 2007 +0200
     2.2 +++ b/src/Pure/type_infer.ML	Thu Aug 30 15:04:44 2007 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4    val paramify_vars: typ -> typ
     2.5    val paramify_dummies: typ -> int -> typ * int
     2.6    val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
     2.7 -  val infer_types: Pretty.pp -> Type.tsig -> Type.mode ->
     2.8 +  val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
     2.9      (string -> typ option) -> (indexname -> typ option) ->
    2.10      Name.context -> bool -> (term * typ) list -> (term * typ) list * (indexname * typ) list
    2.11  end;
    2.12 @@ -381,13 +381,12 @@
    2.13  
    2.14  (* infer_types *)
    2.15  
    2.16 -fun infer_types pp tsig mode const_type var_type used freeze args =
    2.17 +fun infer_types pp tsig check_typs const_type var_type used freeze args =
    2.18    let
    2.19 -    (*certify types*)
    2.20 -    fun certT T = Type.cert_typ_mode mode tsig T;
    2.21 +    (*check types*)
    2.22      val (raw_ts, raw_Ts) = split_list args;
    2.23 -    val ts = map (Term.map_types certT) raw_ts;
    2.24 -    val Ts = map certT raw_Ts;
    2.25 +    val ts = burrow_types check_typs raw_ts;
    2.26 +    val Ts = check_typs raw_Ts;
    2.27  
    2.28      (*constrain vars*)
    2.29      val get_type = the_default dummyT o var_type;