# HG changeset patch
# User wenzelm
# Date 1273767730 -7200
# Node ID 5caff17a28cd0ff6c5f95d37453b26ee5cc6e48d
# Parent  7699f7fafde7be31979d82e5be2924fd351b2565
unconstrainT operations on proofs, according to krauss/schropp;

diff -r 7699f7fafde7 -r 5caff17a28cd src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu May 13 17:25:53 2010 +0200
+++ b/src/Pure/proofterm.ML	Thu May 13 18:22:10 2010 +0200
@@ -1379,6 +1379,31 @@
         fulfill_norm_proof thy (map (apsnd Future.join) promises) body);
 
 
+(***** abstraction over sort constraints *****)
+
+fun unconstrainT_proof thy atyp_map constraints =
+  let
+    fun hyp_map hyp =
+      (case AList.lookup (op =) constraints hyp of
+        SOME t => Hyp t
+      | NONE => raise Fail "unconstrainT_proof: missing constraint");
+
+    val typ = Type.strip_sorts o atyp_map;
+    fun ofclass (ty, c) =
+      let val ty' = Term.map_atyps atyp_map ty;
+      in the_single (of_sort_proof thy hyp_map (ty', [c])) end;
+  in
+    Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass)
+    #> fold_rev (implies_intr_proof o snd) constraints
+  end;
+
+fun unconstrainT_body thy atyp_map constraints (PBody {oracles, thms, proof}) =
+  PBody
+   {oracles = oracles,  (* FIXME unconstrain (!?!) *)
+    thms = thms,
+    proof = unconstrainT_proof thy atyp_map constraints proof};
+
+
 (***** theorems *****)
 
 fun thm_proof thy name hyps concl promises body =