"prep_const" now calls compress_type to ensure sharing among
types of constants in theories.

--- 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;