# HG changeset patch
# User wenzelm
# Date 1564388772 -7200
# Node ID 52fbcf7a61f8be1b4a33fd3c27da38e6114e7245
# Parent  495881aadbff5f5181e48102f180f2c9e14c24b0
tuned signature;

diff -r 495881aadbff -r 52fbcf7a61f8 src/HOL/Types_To_Sets/internalize_sort.ML
--- a/src/HOL/Types_To_Sets/internalize_sort.ML	Sun Jul 28 15:39:30 2019 +0200
+++ b/src/HOL/Types_To_Sets/internalize_sort.ML	Mon Jul 29 10:26:12 2019 +0200
@@ -31,7 +31,8 @@
     val thy = Thm.theory_of_thm thm;
     val tvar = Thm.typ_of ctvar;
 
-    val ((_, assms, classes),_) = Logic.unconstrainT [] (Thm.prop_of thm);
+    val {constraints = assms, outer_constraints = classes, ...} =
+      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)) =
diff -r 495881aadbff -r 52fbcf7a61f8 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Jul 28 15:39:30 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Jul 29 10:26:12 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') =
+    val {atyp_map, constraints, prop = 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
diff -r 495881aadbff -r 52fbcf7a61f8 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Sun Jul 28 15:39:30 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Mon Jul 29 10:26:12 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 495881aadbff -r 52fbcf7a61f8 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sun Jul 28 15:39:30 2019 +0200
+++ b/src/Pure/logic.ML	Mon Jul 29 10:26:12 2019 +0200
@@ -57,7 +57,10 @@
   val mk_arity: string * sort list * class -> term
   val dest_arity: term -> string * sort list * class
   val unconstrainT: sort list -> term ->
-    ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
+   {atyp_map: typ -> typ,
+    constraints: ((typ * class) * term) list,
+    outer_constraints: (typ * class) list,
+    prop: term}
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
@@ -374,7 +377,12 @@
       prop
       |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
       |> curry list_implies (map snd constraints);
-  in ((atyp_map, constraints, outer_constraints), prop') end;
+  in
+   {atyp_map = atyp_map,
+    constraints = constraints,
+    outer_constraints = outer_constraints,
+    prop = prop'}
+  end;
 
 
 
diff -r 495881aadbff -r 52fbcf7a61f8 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Jul 28 15:39:30 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 29 10:26:12 2019 +0200
@@ -1719,7 +1719,8 @@
     val prop = Logic.list_implies (hyps, concl);
     val args = prop_args prop;
 
-    val ((atyp_map, constraints, outer_constraints), prop1) = Logic.unconstrainT shyps prop;
+    val {atyp_map, constraints, outer_constraints, prop = 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;
@@ -1771,7 +1772,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 ""
     | _ => "")