# HG changeset patch
# User paulson
# Date 819625107 -3600
# Node ID f59857e3297236598552db68718f0d8c95b94212
# Parent  cef540a0a10e22dacc1c10ecdb12a749ec616b1f
Commented the datatype declaration of thm.

Declared compress: thm -> thm to copy a thm and maximize sharing in it.

"ext_axms" now calls Term.compress_term so that stored axioms use sharing.

diff -r cef540a0a10e -r f59857e32972 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 22 10:34:54 1995 +0100
+++ b/src/Pure/thm.ML	Fri Dec 22 10:38:27 1995 +0100
@@ -99,6 +99,7 @@
 
   (*meta rules*)
   val assume            : cterm -> thm
+  val compress          : thm -> thm
   val implies_intr      : cterm -> thm -> thm
   val implies_elim      : thm -> thm -> thm
   val forall_intr       : cterm -> thm -> thm
@@ -246,10 +247,12 @@
 
 (*** Meta theorems ***)
 
-(* FIXME comment *)
 datatype thm = Thm of
-  {sign: Sign.sg, maxidx: int,
-    shyps: sort list, hyps: term list, prop: term};
+  {sign: Sign.sg,		(*signature for hyps and prop*)
+   maxidx: int,			(*maximum index of any Var or TVar*)
+   shyps: sort list,		(* FIXME comment *)
+   hyps: term list,		(*hypotheses*)
+   prop: term};			(*conclusion*)
 
 fun rep_thm (Thm args) = args;
 
@@ -328,6 +331,16 @@
   shyps \\ add_thm_sorts (th, []);
 
 
+(*Compression of theorems -- a separate rule, not integrated with the others,
+  as it could be slow.*)
+fun compress (Thm {sign, maxidx, shyps, hyps, prop}) = 
+    Thm {sign = sign, 
+	 maxidx = maxidx,
+	 shyps = shyps, 
+	 hyps = map Term.compress_term hyps, 
+	 prop = Term.compress_term prop};
+
+
 (* fix_shyps *)
 
 (*preserve sort contexts of rule premises and substituted types*)
@@ -528,7 +541,9 @@
 fun ext_axms prep_axm axms (thy as Theory {sign, ...}) =
   let
     val sign1 = Sign.make_draft sign;
-    val axioms = map (apsnd Logic.varify o prep_axm sign) axms;
+    val axioms = map (apsnd (Term.compress_term o Logic.varify) o 
+		      prep_axm sign) 
+	         axms;
   in
     ext_thy thy sign1 axioms
   end;