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

     2.1 --- a/src/Pure/ROOT.ML	Wed Jul 13 20:36:18 2011 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Wed Jul 13 21:44:15 2011 +0200
     2.3 @@ -140,13 +140,13 @@
     2.4  use "primitive_defs.ML";
     2.5  use "defs.ML";
     2.6  use "sign.ML";
     2.7 +use "term_sharing.ML";
     2.8  use "pattern.ML";
     2.9  use "unify.ML";
    2.10  use "theory.ML";
    2.11  use "interpretation.ML";
    2.12  use "proofterm.ML";
    2.13  use "thm.ML";
    2.14 -use "term_sharing.ML";
    2.15  use "more_thm.ML";
    2.16  use "facts.ML";
    2.17  use "global_theory.ML";

     3.1 --- a/src/Pure/proofterm.ML	Wed Jul 13 20:36:18 2011 +0200
     3.2 +++ b/src/Pure/proofterm.ML	Wed Jul 13 21:44:15 2011 +0200
     3.3 @@ -1048,15 +1048,17 @@
     3.4    if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
     3.5    else ((name, prop), gen_axm_proof Oracle name prop);
     3.6  
     3.7 -val shrink_proof =
     3.8 +fun shrink_proof thy =
     3.9    let
    3.10 +    val (typ, term) = Term_Sharing.init thy;
    3.11 +
    3.12      fun shrink ls lev (prf as Abst (a, T, body)) =
    3.13            let val (b, is, ch, body') = shrink ls (lev+1) body
    3.14 -          in (b, is, ch, if ch then Abst (a, T, body') else prf) end
    3.15 +          in (b, is, ch, if ch then Abst (a, Option.map typ T, body') else prf) end
    3.16        | shrink ls lev (prf as AbsP (a, t, body)) =
    3.17            let val (b, is, ch, body') = shrink (lev::ls) lev body
    3.18            in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is,
    3.19 -            ch, if ch then AbsP (a, t, body') else prf)
    3.20 +            ch, if ch then AbsP (a, Option.map term t, body') else prf)
    3.21            end
    3.22        | shrink ls lev prf =
    3.23            let val (is, ch, _, prf') = shrink' ls lev [] [] prf
    3.24 @@ -1071,13 +1073,13 @@
    3.25        | shrink' ls lev ts prfs (prf as prf1 % t) =
    3.26            let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
    3.27            in (is, ch orelse ch', ts',
    3.28 -              if ch orelse ch' then prf' % t' else prf) end
    3.29 +              if ch orelse ch' then prf' % Option.map term t' else prf) end
    3.30        | shrink' ls lev ts prfs (prf as PBound i) =
    3.31            (if exists (fn SOME (Bound j) => lev-j <= nth ls i | _ => true) ts
    3.32               orelse has_duplicates (op =)
    3.33                 (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
    3.34               orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
    3.35 -      | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf)
    3.36 +      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (term t))
    3.37        | shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf)
    3.38        | shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf)
    3.39        | shrink' ls lev ts prfs prf =
    3.40 @@ -1442,7 +1444,7 @@
    3.41      val argsP = map OfClass outer_constraints @ map Hyp hyps;
    3.42  
    3.43      fun full_proof0 () =
    3.44 -      #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
    3.45 +      #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
    3.46  
    3.47      fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    3.48      val body0 =

     4.1 --- a/src/Pure/thm.ML	Wed Jul 13 20:36:18 2011 +0200
     4.2 +++ b/src/Pure/thm.ML	Wed Jul 13 21:44:15 2011 +0200
     4.3 @@ -106,6 +106,7 @@
     4.4    val axioms_of: theory -> (string * thm) list
     4.5    val get_tags: thm -> Properties.T
     4.6    val map_tags: (Properties.T -> Properties.T) -> thm -> thm
     4.7 +  val compress: thm -> thm
     4.8    val norm_proof: thm -> thm
     4.9    val adjust_maxidx_thm: int -> thm -> thm
    4.10    (*meta rules*)
    4.11 @@ -630,6 +631,26 @@
    4.12      shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop});
    4.13  
    4.14  
    4.15 +(* technical adjustments *)
    4.16 +
    4.17 +fun compress (Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
    4.18 +  let
    4.19 +    val thy = Theory.deref thy_ref;
    4.20 +    val term = #2 (Term_Sharing.init thy);
    4.21 +    val hyps' = map term hyps;
    4.22 +    val tpairs' = map (pairself term) tpairs;
    4.23 +    val prop' = term prop;
    4.24 +  in
    4.25 +    Thm (der,
    4.26 +     {thy_ref = Theory.check_thy thy,
    4.27 +      tags = tags,
    4.28 +      maxidx = maxidx,
    4.29 +      shyps = shyps,
    4.30 +      hyps = hyps',
    4.31 +      tpairs = tpairs',
    4.32 +      prop = prop'})
    4.33 +  end;
    4.34 +
    4.35  fun norm_proof (Thm (der, args as {thy_ref, ...})) =
    4.36    let
    4.37      val thy = Theory.deref thy_ref;