# HG changeset patch
# User wenzelm
# Date 1703967731 -3600
# Node ID 27e1cd1bba7630092c6b76c51b4969993b95e724
# Parent  70c0dbfacf0bdcaa4ef4ced9929b6b09303583dc
tuned;

diff -r 70c0dbfacf0b -r 27e1cd1bba76 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Dec 30 17:19:31 2023 +0100
+++ b/src/Pure/proofterm.ML	Sat Dec 30 21:22:11 2023 +0100
@@ -2142,9 +2142,11 @@
     val typ = #unconstrain_typ ucontext {strip_sorts = true};
     val typ_sort = #unconstrain_typ ucontext {strip_sorts = false};
 
-    fun ofclass (ty, c) =
-      let val ty' = Same.commit typ_sort ty;
-      in the_single (of_sort_proof algebra classrel_proof arity_proof hyp_map (ty', [c])) end;
+    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)