proper treatment of sorts;

--- a/src/Pure/proofterm.ML	Tue Oct 08 16:04:59 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Oct 08 16:11:04 2019 +0200
@@ -1576,14 +1576,14 @@
 
 fun app_types shift prop Ts prf =
   let
-    val tvars = rev (Term.add_tvars prop []) |> map #1;
-    val tfrees = rev (Term.add_tfrees prop []) |> map (fn (a, _) => (a, ~1));
+    val tvars = rev (Term.add_tvars prop []);
+    val tfrees = rev (Term.add_tfrees prop []) |> map (fn (a, S) => ((a, ~1), S));
     val inst = (tvars @ tfrees) ~~ Ts;
     fun subst_same v = (case AList.lookup (op =) inst v of SOME T => T | NONE => raise Same.SAME);
     val subst_type_same =
       Term_Subst.map_atypsT_same
-        (fn TVar ((a, i), _) => subst_same (a, i - shift)
-          | TFree (a, _) => subst_same (a, ~1));
+        (fn TVar ((a, i), S) => subst_same ((a, i - shift), S)
+          | TFree (a, S) => subst_same ((a, ~1), S));
   in Same.commit (map_proof_types_same subst_type_same) prf end;
 
 fun guess_name (PThm ({name, ...}, _)) = name