src/Pure/proofterm.ML

--- a/src/Pure/proofterm.ML	Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/proofterm.ML	Sun Dec 31 22:04:41 2023 +0100
@@ -1654,7 +1654,7 @@
         (case Sign.const_type thy s of
           NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
         | SOME T =>
-            let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) in
+            let val T' = Term.strip_sortsT (Logic.incr_tvar (maxidx + 1) T) in
               (Const (s, T'), T', vTs,
                 Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
             end)