# HG changeset patch
# User wenzelm
# Date 1564391377 -7200
# Node ID 251f1fb44ccd26beb6e6c1ddddc338afe920c96a
# Parent  52fbcf7a61f8be1b4a33fd3c27da38e6114e7245
clarified signature;
tuned;

diff -r 52fbcf7a61f8 -r 251f1fb44ccd src/HOL/Types_To_Sets/internalize_sort.ML
--- a/src/HOL/Types_To_Sets/internalize_sort.ML	Mon Jul 29 10:26:12 2019 +0200
+++ b/src/HOL/Types_To_Sets/internalize_sort.ML	Mon Jul 29 11:09:37 2019 +0200
@@ -31,15 +31,14 @@
     val thy = Thm.theory_of_thm thm;
     val tvar = Thm.typ_of ctvar;
 
-    val {constraints = assms, outer_constraints = classes, ...} =
-      Logic.unconstrainT [] (Thm.prop_of thm);
+    val (ucontext, _) = Logic.unconstrainT [] (Thm.prop_of thm);
 
     fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
     fun reduce_to_non_proper_sort (TVar (name, sort)) =
         TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
       | reduce_to_non_proper_sort _ = error "not supported";
 
-    val data = (map fst classes) ~~ assms;
+    val data = map #1 (#outer_constraints ucontext) ~~ #constraints ucontext;
 
     val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
       then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
diff -r 52fbcf7a61f8 -r 251f1fb44ccd src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Jul 29 11:09:37 2019 +0200
@@ -365,7 +365,7 @@
 fun abs_corr_shyps thy thm vs xs prf =
   let
     val S = Sign.defaultS thy;
-    val {atyp_map, constraints, prop = prop', ...} =
+    val (ucontext, prop') =
       Logic.unconstrainT (Thm.shyps_of thm) (Thm.prop_of thm);
     val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
     val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
@@ -374,13 +374,13 @@
     val cs = maps (fn T => map (pair T) S) Ts;
     val constraints' = map Logic.mk_of_class cs;
     fun typ_map T = Type.strip_sorts
-      (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
+      (map_atyps (fn U => if member (op =) atyps U then (#atyp_map ucontext) U else U) T);
     fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
     val xs' = map (map_types typ_map) xs
   in
     prf |>
     Same.commit (Proofterm.map_proof_same (map_types typ_map) typ_map mk_hyp) |>
-    fold_rev Proofterm.implies_intr_proof' (map snd constraints) |>
+    fold_rev Proofterm.implies_intr_proof' (map snd (#constraints ucontext)) |>
     fold_rev Proofterm.forall_intr_proof' xs' |>
     fold_rev Proofterm.implies_intr_proof' constraints'
   end;
diff -r 52fbcf7a61f8 -r 251f1fb44ccd src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Mon Jul 29 11:09:37 2019 +0200
@@ -379,7 +379,7 @@
 
 fun clean_proof_of ctxt full thm =
   let
-    val {prop, ...} =
+    val (_, prop) =
       Logic.unconstrainT (Thm.shyps_of thm)
         (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
   in
diff -r 52fbcf7a61f8 -r 251f1fb44ccd src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/logic.ML	Mon Jul 29 11:09:37 2019 +0200
@@ -56,11 +56,13 @@
   val mk_arities: arity -> term list
   val mk_arity: string * sort list * class -> term
   val dest_arity: term -> string * sort list * class
-  val unconstrainT: sort list -> term ->
-   {atyp_map: typ -> typ,
+  type unconstrain_context =
+   {present_map: (typ * typ) list,
+    extra_map: (sort * typ) list,
+    atyp_map: typ -> typ,
     constraints: ((typ * class) * term) list,
-    outer_constraints: (typ * class) list,
-    prop: term}
+    outer_constraints: (typ * class) list};
+  val unconstrainT: sort list -> term -> unconstrain_context * term
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
@@ -342,6 +344,13 @@
 
 (* internalized sort constraints *)
 
+type unconstrain_context =
+ {present_map: (typ * typ) list,
+  extra_map: (sort * typ) list,
+  atyp_map: typ -> typ,
+  constraints: ((typ * class) * term) list,
+  outer_constraints: (typ * class) list};
+
 fun unconstrainT shyps prop =
   let
     val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
@@ -352,37 +361,37 @@
 
     val present_map =
       map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
-    val constraints_map =
-      map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
+    val extra_map =
       map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
 
     fun atyp_map T =
       (case AList.lookup (op =) present_map T of
         SOME U => U
       | NONE =>
-          (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
+          (case AList.lookup (op =) extra_map (Type.sort_of_atyp T) of
             SOME U => U
           | NONE => raise TYPE ("Dangling type variable", [T], [])));
 
+    val constraints_map =
+      map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @ extra_map;
     val constraints =
-      maps (fn (_, T as TVar (ai, S)) =>
-        map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
-        constraints_map;
+      constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
+        map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S);
 
     val outer_constraints =
       maps (fn (T, S) => map (pair T) S)
         (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
 
-    val prop' =
-      prop
+    val context =
+     {present_map = present_map,
+      extra_map = extra_map,
+      atyp_map = atyp_map,
+      constraints = constraints,
+      outer_constraints = outer_constraints};
+    val prop' = prop
       |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
       |> curry list_implies (map snd constraints);
-  in
-   {atyp_map = atyp_map,
-    constraints = constraints,
-    outer_constraints = outer_constraints,
-    prop = prop'}
-  end;
+  in (context, prop') end;
 
 
 
diff -r 52fbcf7a61f8 -r 251f1fb44ccd src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 29 11:09:37 2019 +0200
@@ -1670,38 +1670,28 @@
 
 
 
-(** abstraction over sort constraints **)
-
-fun unconstrainT_prf thy (atyp_map, constraints) =
-  let
-    fun hyp_map hyp =
-      (case AList.lookup (op =) constraints hyp of
-        SOME t => Hyp t
-      | NONE => raise Fail "unconstrainT_prf: missing constraint");
-
-    val typ = Term_Subst.map_atypsT_same (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 constrs (PBody {oracles, thms, proof}) =
-  PBody
-   {oracles = oracles,  (* FIXME merge (!), unconstrain (!?!) *)
-    thms = thms,  (* FIXME merge (!) *)
-    proof = unconstrainT_prf thy constrs proof};
-
-
-
 (** theorems **)
 
 val proof_serial = Counter.make ();
 
 local
 
+fun unconstrainT_prf thy (ucontext: Logic.unconstrain_context) =
+  let
+    fun hyp_map hyp =
+      (case AList.lookup (op =) (#constraints ucontext) hyp of
+        SOME t => Hyp t
+      | NONE => raise Fail "unconstrainT_prf: missing constraint");
+
+    val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o #atyp_map ucontext);
+    fun ofclass (ty, c) =
+      let val ty' = Term.map_atyps (#atyp_map ucontext) 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 ucontext)
+  end;
+
 fun export thy i proof =
   if Options.default_bool "export_proofs" then
     Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i]))
@@ -1719,12 +1709,11 @@
     val prop = Logic.list_implies (hyps, concl);
     val args = prop_args prop;
 
-    val {atyp_map, constraints, outer_constraints, prop = prop1, ...} =
-      Logic.unconstrainT shyps prop;
+    val (ucontext, prop1) = Logic.unconstrainT shyps prop;
     val args1 =
       (map o Option.map o Term.map_types o Term.map_atyps)
-        (Type.strip_sorts o atyp_map) args;
-    val argsP = map OfClass outer_constraints @ map Hyp hyps;
+        (Type.strip_sorts o #atyp_map ucontext) args;
+    val argsP = map OfClass (#outer_constraints ucontext) @ map Hyp hyps;
 
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
     val body0 =
@@ -1738,7 +1727,7 @@
     fun new_prf () =
       let
         val i = proof_serial ();
-        val postproc = unconstrainT_body thy (atyp_map, constraints) #> named ? publish i;
+        val postproc = map_proof_of (unconstrainT_prf thy ucontext) #> named ? publish i;
       in (i, fulfill_proof_future thy promises postproc body0) end;
 
     val (i, body') =
@@ -1772,7 +1761,7 @@
 (* approximative PThm name *)
 
 fun get_name shyps hyps prop prf =
-  let val {prop, ...} = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
+  let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
     (case strip_combt (fst (strip_combP prf)) of
       (PThm (_, ((name, prop', _, _), _)), _) => if prop = prop' then name else ""
     | _ => "")