# HG changeset patch # User wenzelm # Date 1273435584 -7200 # Node ID c3a04614c710829de6cdfd8838173c5c1c8a719a # Parent b6b88bf695b3640de15bbc58ec7e45d08eb137dd reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv; diff -r b6b88bf695b3 -r c3a04614c710 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun May 09 19:50:56 2010 +0200 +++ b/src/Pure/thm.ML Sun May 09 22:06:24 2010 +0200 @@ -139,6 +139,7 @@ val of_class: ctyp * class -> thm val strip_shyps: thm -> thm val unconstrainT: thm -> thm + val legacy_unconstrainT: ctyp -> thm -> thm val legacy_freezeT: thm -> thm val assumption: int -> thm -> thm Seq.seq val eq_assumption: int -> thm -> thm @@ -1242,6 +1243,26 @@ prop = prop'}) end; +fun legacy_unconstrainT + (Ctyp {thy_ref = thy_ref1, T, ...}) + (th as Thm (_, {thy_ref = thy_ref2, maxidx, shyps, hyps, tpairs, prop, ...})) = + let + val ((x, i), S) = Term.dest_TVar T handle TYPE _ => + raise THM ("unconstrainT: not a type variable", 0, [th]); + val T' = TVar ((x, i), []); + val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U)); + val constraints = Logic.mk_of_sort (T', S); + in + Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])), + {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), + tags = [], + maxidx = Int.max (maxidx, i), + shyps = Sorts.remove_sort S shyps, + hyps = hyps, + tpairs = map (pairself unconstrain) tpairs, + prop = Logic.list_implies (constraints, unconstrain prop)}) + end; + (* Replace all TFrees not fixed or in the hyps by new TVars *) fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = diff -r b6b88bf695b3 -r c3a04614c710 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sun May 09 19:50:56 2010 +0200 +++ b/src/Tools/nbe.ML Sun May 09 22:06:24 2010 +0200 @@ -101,16 +101,16 @@ val prem_thms = map (the o AList.lookup (op =) of_classes o apfst (fst o fst o dest_TVar) o Logic.dest_of_class) prem_props; in Drule.implies_elim_list thm prem_thms end; - in ct + in + (* FIXME avoid legacy operations *) + ct |> Drule.cterm_rule Thm.varifyT_global |> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) => (((v, 0), sort), TFree (v, sort'))) vs, [])) |> Drule.cterm_rule Thm.legacy_freezeT |> conv |> Thm.varifyT_global -(* FIXME tmp *) -(* |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs*) - |> Thm.unconstrainT + |> fold (fn (v, (_, sort')) => Thm.legacy_unconstrainT (certT (TVar ((v, 0), sort')))) vs |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) => (((v, 0), []), TVar ((v, 0), sort))) vs, []) |> strip_of_class