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