# HG changeset patch
# User paulson
# Date 819624606 -3600
# Node ID 036e072b215a182f1c53a6f326d8f780a9dbd946
# Parent  73fac49f608f2dacf8b02d09e63cf455aa6d2145
"prep_const" now calls compress_type to ensure sharing among
types of constants in theories.

diff -r 73fac49f608f -r 036e072b215a src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Dec 22 10:26:57 1995 +0100
+++ b/src/Pure/sign.ML	Fri Dec 22 10:30:06 1995 +0100
@@ -405,7 +405,10 @@
 
 fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   let
-    fun prep_const (c, ty, mx) = (c, varifyT (cert_typ tsig (no_tvars ty)), mx)
+    fun prep_const (c, ty, mx) = 
+	  (c, 
+	   compress_type (varifyT (cert_typ tsig (no_tvars ty))), 
+	   mx)
       handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
 
     val consts = map (prep_const o rd_const syn tsig) raw_consts;