tuned signature;

--- a/src/Pure/proofterm.ML	Mon Mar 09 13:03:42 2020 +0100
+++ b/src/Pure/proofterm.ML	Mon Mar 09 14:13:44 2020 +0100
@@ -1064,7 +1064,7 @@
 
 fun strip_shyps_proof algebra present witnessed extra_sorts prf =
   let
-    fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
+    fun get S (T', S') = if Sorts.sort_le algebra (S', S) then SOME T' else NONE;
     val extra = map (`Logic.dummy_tfree) extra_sorts;
     val replacements = present @ extra @ witnessed;
     fun replace T =