1.1 --- a/src/Pure/thm.ML	Wed May 19 10:14:37 2010 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed May 19 10:17:05 2010 +0200
     1.3 @@ -139,7 +139,6 @@
     1.4    val of_class: ctyp * class -> thm
     1.5    val strip_shyps: thm -> thm
     1.6    val unconstrainT: thm -> thm
     1.7 -  val legacy_unconstrainT: ctyp -> thm -> thm
     1.8    val legacy_freezeT: thm -> thm
     1.9    val assumption: int -> thm -> thm Seq.seq
    1.10    val eq_assumption: int -> thm -> thm
    1.11 @@ -1249,27 +1248,6 @@
    1.12        prop = prop'})
    1.13    end;
    1.14  
    1.15 -fun legacy_unconstrainT
    1.16 -    (Ctyp {thy_ref = thy_ref1, T, ...})
    1.17 -    (th as Thm (_, {thy_ref = thy_ref2, maxidx, shyps, hyps, tpairs, prop, ...})) =
    1.18 -  let
    1.19 -    val ((x, i), S) = Term.dest_TVar T handle TYPE _ =>
    1.20 -      raise THM ("unconstrainT: not a type variable", 0, [th]);
    1.21 -    val T' = TVar ((x, i), []);
    1.22 -    val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
    1.23 -    val constraints = Logic.mk_of_sort (T', S);
    1.24 -  in
    1.25 -    Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
    1.26 -     {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
    1.27 -      tags = [],
    1.28 -      maxidx = Int.max (maxidx, i),
    1.29 -      shyps = Sorts.remove_sort S shyps,
    1.30 -      hyps = hyps,
    1.31 -      tpairs = map (pairself unconstrain) tpairs,
    1.32 -      prop = Logic.list_implies (constraints, unconstrain prop)})
    1.33 -  end;
    1.34 -
    1.35 -
    1.36  (* Replace all TFrees not fixed or in the hyps by new TVars *)
    1.37  fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
    1.38    let