# HG changeset patch
# User wenzelm
# Date 1360766459 -3600
# Node ID 18daa3380ff7699e8cb4079593c4645eb63563b9
# Parent  2ef891f99d2c6f45faadf4bea6697fb6550058d9
discontinued home-made sharing for proof terms -- leave memory management to the Poly/ML RTS;

diff -r 2ef891f99d2c -r 18daa3380ff7 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Feb 13 13:52:06 2013 +0100
+++ b/src/Pure/proofterm.ML	Wed Feb 13 15:40:59 2013 +0100
@@ -1057,15 +1057,13 @@
 
 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, Option.map typ T, body') else prf) end
+          in (b, is, ch, if ch then Abst (a, 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, Option.map term t, body') else prf)
+            ch, if ch then AbsP (a, t, body') else prf)
           end
       | shrink ls lev prf =
           let val (is, ch, _, prf') = shrink' ls lev [] [] prf
@@ -1080,13 +1078,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' % Option.map term t' else prf) end
+              if ch orelse ch' then prf' % 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 (Hyp t) = ([], false, map (pair false) ts, Hyp (term t))
+      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp 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 =