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.
Compress.typ;
authorwenzelm
Mon, 01 Aug 2005 19:20:42 +0200
changeset 16988 02cd0c8b96d9
parent 16987 9ed901d738ba
child 16989 1877b00fb4d2
Compress.typ;
src/Pure/sign.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/sign.ML	Mon Aug 01 19:20:41 2005 +0200
+++ b/src/Pure/sign.ML	Mon Aug 01 19:20:42 2005 +0200
@@ -672,7 +672,7 @@
 
 fun gen_add_consts prep_typ raw_args thy =
   let
-    val prepT = compress_type o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
+    val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
     fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
       handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
     val args = map prep raw_args;
isabelle