src/Pure/type.ML
changeset 12314 160013745a92
parent 12222 d1c276b45dbc
child 12501 36b2ac65e18d
     1.1 --- a/src/Pure/type.ML	Wed Nov 28 23:28:58 2001 +0100
     1.2 +++ b/src/Pure/type.ML	Wed Nov 28 23:29:21 2001 +0100
     1.3 @@ -868,7 +868,7 @@
     1.4      val sort_of = get_sort tsig def_sort map_sort raw_env;
     1.5  
     1.6      val certT = cert_typ tsig o map_type;
     1.7 -    fun decodeT t = certT (Syntax.typ_of_term sort_of t);
     1.8 +    fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t);
     1.9  
    1.10      fun decode (Const ("_constrain", _) $ t $ typ) =
    1.11            constrain (decode t) (decodeT typ)