src/Pure/thm.ML

--- a/src/Pure/thm.ML	Thu May 13 21:36:38 2010 +0200
+++ b/src/Pure/thm.ML	Fri May 14 19:53:36 2010 +0200
@@ -1222,24 +1222,30 @@
       end;
 
 (*Internalize sort constraints of type variables*)
-fun unconstrainT (thm as Thm (_, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
+fun unconstrainT (thm as Thm (der, args)) =
   let
+    val Deriv {promises, body} = der;
+    val {thy_ref, shyps, hyps, tpairs, prop, ...} = args;
+
     fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]);
-
     val _ = null hyps orelse err "illegal hyps";
     val _ = null tpairs orelse err "unsolved flex-flex constraints";
     val tfrees = rev (Term.add_tfree_names prop []);
     val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
 
-    val (_, prop') = Logic.unconstrainT shyps prop;
+    val ps = map (apsnd (Future.map proof_body_of)) promises;
+    val thy = Theory.deref thy_ref;
+    val (pthm as (_, (_, prop', _)), proof) = Pt.unconstrain_thm_proof thy shyps prop ps body;
+    val der' = make_deriv [] [] [pthm] proof;
+    val _ = Theory.check_thy thy;
   in
-    Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
+    Thm (der',
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx_of_term prop',
       shyps = [[]],  (*potentially redundant*)
-      hyps = hyps,
-      tpairs = tpairs,
+      hyps = [],
+      tpairs = [],
       prop = prop'})
   end;