# HG changeset patch
# User wenzelm
# Date 1704022393 -3600
# Node ID 254b062ec54dac5e31df11ef60f7a30f47d1a743
# Parent  6bcb7131142d9be8b434ec29571f514a7dacd28e
tuned structure;

diff -r 6bcb7131142d -r 254b062ec54d src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Dec 31 12:22:23 2023 +0100
+++ b/src/Pure/proofterm.ML	Sun Dec 31 12:33:13 2023 +0100
@@ -1106,6 +1106,26 @@
       in proof_combP (arity_proof (a, Ss, c), prfs) end,
     type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)};
 
+fun unconstrainT_proof algebra classrel_proof arity_proof (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_proof: missing constraint");
+
+    val typ = #unconstrain_typ ucontext {strip_sorts = true};
+    val typ_sort = #unconstrain_typ ucontext {strip_sorts = false};
+
+    fun ofclass (T, c) =
+      let
+        val T' = Same.commit typ_sort T;
+        val [p] = of_sort_proof algebra classrel_proof arity_proof hyp_map (T', [c])
+      in p 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;
+
 
 
 (** axioms and theorems **)
@@ -2131,26 +2151,6 @@
 
 local
 
-fun unconstrainT_proof algebra classrel_proof arity_proof (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_proof: missing constraint");
-
-    val typ = #unconstrain_typ ucontext {strip_sorts = true};
-    val typ_sort = #unconstrain_typ ucontext {strip_sorts = false};
-
-    fun ofclass (T, c) =
-      let
-        val T' = Same.commit typ_sort T;
-        val [p] = of_sort_proof algebra classrel_proof arity_proof hyp_map (T', [c])
-      in p 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_proof thy i prop prf0 =
   let
     val prf = prf0