recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;

--- a/src/Pure/Isar/generic_target.ML	Wed Jul 13 20:36:18 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Jul 13 21:44:15 2011 +0200
@@ -118,7 +118,7 @@
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
-    val result = Global_Theory.name_thm true true name th'';
+    val result = Global_Theory.name_thm true true name (Thm.compress th'');
 
     (*import fixes*)
     val (tvars, vars) =

--- a/src/Pure/ROOT.ML	Wed Jul 13 20:36:18 2011 +0200
+++ b/src/Pure/ROOT.ML	Wed Jul 13 21:44:15 2011 +0200
@@ -140,13 +140,13 @@
 use "primitive_defs.ML";
 use "defs.ML";
 use "sign.ML";
+use "term_sharing.ML";
 use "pattern.ML";
 use "unify.ML";
 use "theory.ML";
 use "interpretation.ML";
 use "proofterm.ML";
 use "thm.ML";
-use "term_sharing.ML";
 use "more_thm.ML";
 use "facts.ML";
 use "global_theory.ML";

--- a/src/Pure/proofterm.ML	Wed Jul 13 20:36:18 2011 +0200
+++ b/src/Pure/proofterm.ML	Wed Jul 13 21:44:15 2011 +0200
@@ -1048,15 +1048,17 @@
   if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
   else ((name, prop), gen_axm_proof Oracle name prop);
 
-val shrink_proof =
+fun shrink_proof thy =
   let
+    val (typ, term) = Term_Sharing.init thy;
+
     fun shrink ls lev (prf as Abst (a, T, body)) =
           let val (b, is, ch, body') = shrink ls (lev+1) body
-          in (b, is, ch, if ch then Abst (a, T, body') else prf) end
+          in (b, is, ch, if ch then Abst (a, Option.map typ T, body') else prf) end
       | shrink ls lev (prf as AbsP (a, t, body)) =
           let val (b, is, ch, body') = shrink (lev::ls) lev body
           in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is,
-            ch, if ch then AbsP (a, t, body') else prf)
+            ch, if ch then AbsP (a, Option.map term t, body') else prf)
           end
       | shrink ls lev prf =
           let val (is, ch, _, prf') = shrink' ls lev [] [] prf
@@ -1071,13 +1073,13 @@
       | shrink' ls lev ts prfs (prf as prf1 % t) =
           let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
           in (is, ch orelse ch', ts',
-              if ch orelse ch' then prf' % t' else prf) end
+              if ch orelse ch' then prf' % Option.map term t' else prf) end
       | shrink' ls lev ts prfs (prf as PBound i) =
           (if exists (fn SOME (Bound j) => lev-j <= nth ls i | _ => true) ts
              orelse has_duplicates (op =)
                (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
              orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
-      | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf)
+      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (term t))
       | shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf)
       | shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf)
       | shrink' ls lev ts prfs prf =
@@ -1442,7 +1444,7 @@
     val argsP = map OfClass outer_constraints @ map Hyp hyps;
 
     fun full_proof0 () =
-      #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
+      #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
 
     fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
     val body0 =

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