Syntax.typ_of_term: pass intern sort fn;
authorwenzelm
Wed Nov 28 23:29:21 2001 +0100 (2001-11-28 ago)
changeset 12314160013745a92
parent 12313 e2cb7e8bb037
child 12315 edeb1bbcd479
Syntax.typ_of_term: pass intern sort fn;
src/Pure/type.ML
     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)