--- a/src/Pure/thm.ML Wed Jul 13 20:36:18 2011 +0200
+++ b/src/Pure/thm.ML Wed Jul 13 21:44:15 2011 +0200
@@ -106,6 +106,7 @@
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*)
@@ -630,6 +631,26 @@
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop});
+(* 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;