--- 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