# HG changeset patch
# User wenzelm
# Date 1006986561 -3600
# Node ID 160013745a9287cf815012fe195601ad1c7633e8
# Parent  e2cb7e8bb03794abc581d5e1cef5a3705c29ab9a
Syntax.typ_of_term: pass intern sort fn;

diff -r e2cb7e8bb037 -r 160013745a92 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Nov 28 23:28:58 2001 +0100
+++ b/src/Pure/type.ML	Wed Nov 28 23:29:21 2001 +0100
@@ -868,7 +868,7 @@
     val sort_of = get_sort tsig def_sort map_sort raw_env;
 
     val certT = cert_typ tsig o map_type;
-    fun decodeT t = certT (Syntax.typ_of_term sort_of t);
+    fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t);
 
     fun decode (Const ("_constrain", _) $ t $ typ) =
           constrain (decode t) (decodeT typ)