--- 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, ...})) =
--- 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