# 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