# HG changeset patch
# User wenzelm
# Date 1273859616 -7200
# Node ID 4ed0d72def502a1e3373507555cb0aba3a71fdd8
# Parent  f33760bb8ca0143e37eff1de0eb53d7de5f2b77d
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;

diff -r f33760bb8ca0 -r 4ed0d72def50 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu May 13 21:36:38 2010 +0200
+++ b/src/Pure/proofterm.ML	Fri May 14 19:53:36 2010 +0200
@@ -135,6 +135,8 @@
   val unconstrain_thm_proofs: bool Unsynchronized.ref
   val thm_proof: theory -> string -> sort list -> term list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
+  val unconstrain_thm_proof: theory -> sort list -> term ->
+    (serial * proof_body future) list -> proof_body -> pthm * proof
   val get_name: term list -> term -> proof -> string
   val get_name_unconstrained: sort list -> term list -> term -> proof -> string
   val guess_name: proof -> string
@@ -1400,16 +1402,14 @@
 
 fun unconstrainT_body thy constrs (PBody {oracles, thms, proof}) =
   PBody
-   {oracles = oracles,  (* FIXME unconstrain (!?!) *)
-    thms = thms,
+   {oracles = oracles,  (* FIXME merge (!), unconstrain (!?!) *)
+    thms = thms,  (* FIXME merge (!) *)
     proof = unconstrainT_prf thy constrs proof};
 
 
 (***** theorems *****)
 
-val unconstrain_thm_proofs = Unsynchronized.ref false;
-
-fun thm_proof thy name shyps hyps concl promises body =
+fun prepare_thm_proof do_unconstrain thy name shyps hyps concl promises body =
   let
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
     val prop = Logic.list_implies (hyps, concl);
@@ -1418,13 +1418,16 @@
         if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
       map SOME (frees_of prop);
 
-    val (postproc, ofclasses, prop1) =
-      if ! unconstrain_thm_proofs then
+    val (postproc, ofclasses, prop1, args1) =
+      if do_unconstrain then
         let
           val ((atyp_map, constraints), prop1) = Logic.unconstrainT shyps prop;
           val postproc = unconstrainT_body thy (atyp_map, constraints);
-        in (postproc, map (OfClass o fst) constraints, prop1) end
-      else (I, [], prop);
+          val args1 =
+            (map o Option.map o Term.map_types o Term.map_atyps)
+              (Type.strip_sorts o atyp_map) args;
+        in (postproc, map (OfClass o fst) constraints, prop1, args1) end
+      else (I, [], prop, args);
     val argsP = ofclasses @ map Hyp hyps;
 
     val proof0 =
@@ -1442,9 +1445,21 @@
           else new_prf ()
       | _ => new_prf ());
     val head = PThm (i, ((name, prop1, NONE), body'));
-  in
-    ((i, (name, prop1, body')), proof_combP (proof_combt' (head, args), argsP))
-  end;
+  in ((i, (name, prop1, body')), head, args, argsP, args1) end;
+
+val unconstrain_thm_proofs = Unsynchronized.ref false;
+
+fun thm_proof thy name shyps hyps concl promises body =
+  let val (pthm, head, args, argsP, _) =
+    prepare_thm_proof (! unconstrain_thm_proofs) thy name shyps hyps concl promises body
+  in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
+
+fun unconstrain_thm_proof thy shyps concl promises body =
+  let
+    val (pthm, head, _, _, args) =
+      prepare_thm_proof true thy "" shyps [] concl promises body
+  in (pthm, proof_combt' (head, args)) end;
+
 
 fun get_name hyps prop prf =
   let val prop = Logic.list_implies (hyps, prop) in
diff -r f33760bb8ca0 -r 4ed0d72def50 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;