Type.cert_typ;
authorwenzelm
Mon Jun 21 16:40:44 2004 +0200 (2004-06-21)
changeset 14988973ced82812d
parent 14987 699239c7632c
child 14989 5a5d076a9863
Type.cert_typ;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Mon Jun 21 16:40:30 2004 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Jun 21 16:40:44 2004 +0200
     1.3 @@ -477,7 +477,7 @@
     1.4      val raw_env = Syntax.raw_term_sorts tm;
     1.5      val sort_of = get_sort tsig def_sort map_sort raw_env;
     1.6  
     1.7 -    val certT = Type.cert_typ tsig o map_type;
     1.8 +    val certT = #1 o Type.cert_typ tsig o map_type;
     1.9      fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t);
    1.10  
    1.11      fun decode (Const ("_constrain", _) $ t $ typ) =
    1.12 @@ -518,7 +518,7 @@
    1.13      map_const map_type map_sort used freeze pat_Ts raw_ts =
    1.14    let
    1.15      val {classes, arities, ...} = Type.rep_tsig tsig;
    1.16 -    val pat_Ts' = map (Type.cert_typ tsig) pat_Ts;
    1.17 +    val pat_Ts' = map (#1 o Type.cert_typ tsig) pat_Ts;
    1.18      val is_const = is_some o const_type;
    1.19      val raw_ts' =
    1.20        map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;