Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Syntax.typ_of_term: pass intern sort fn;
authorwenzelm
Wed, 28 Nov 2001 23:29:21 +0100
changeset 12314 160013745a92
parent 12313 e2cb7e8bb037
child 12315 edeb1bbcd479
Syntax.typ_of_term: pass intern sort fn;
src/Pure/type.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle