# HG changeset patch
# User wenzelm
# Date 1320943296 -3600
# Node ID c8a9a5e577bdc75d37a7007744fb481cee8825fe
# Parent  2b91e27676b257800413d07c716c93a9e98d60dd
discontinued unused Thm.compress (again);

diff -r 2b91e27676b2 -r c8a9a5e577bd src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Nov 10 17:28:02 2011 +0100
+++ b/src/Pure/thm.ML	Thu Nov 10 17:41:36 2011 +0100
@@ -107,7 +107,6 @@
   val axioms_of: theory -> (string * thm) list
   val get_tags: thm -> Properties.T
   val map_tags: (Properties.T -> Properties.T) -> thm -> thm
-  val compress: thm -> thm
   val norm_proof: thm -> thm
   val adjust_maxidx_thm: int -> thm -> thm
   (*meta rules*)
@@ -646,24 +645,6 @@
 
 (* technical adjustments *)
 
-fun compress (Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
-  let
-    val thy = Theory.deref thy_ref;
-    val term = #2 (Term_Sharing.init thy);
-    val hyps' = map term hyps;
-    val tpairs' = map (pairself term) tpairs;
-    val prop' = term prop;
-  in
-    Thm (der,
-     {thy_ref = Theory.check_thy thy,
-      tags = tags,
-      maxidx = maxidx,
-      shyps = shyps,
-      hyps = hyps',
-      tpairs = tpairs',
-      prop = prop'})
-  end;
-
 fun norm_proof (Thm (der, args as {thy_ref, ...})) =
   let
     val thy = Theory.deref thy_ref;