--- a/src/Pure/raw_simplifier.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/raw_simplifier.ML Fri Sep 10 14:59:19 2021 +0200
@@ -1226,7 +1226,8 @@
val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
val eq' =
Thm.implies_elim
- (Thm.instantiate ([], [(vA, prem), (vB, lhs), (vC, rhs)]) Drule.imp_cong)
+ (Thm.instantiate (TVars.empty, Vars.make [(vA, prem), (vB, lhs), (vC, rhs)])
+ Drule.imp_cong)
(Thm.implies_intr prem eq);
in
if not r then eq'
@@ -1237,9 +1238,11 @@
in
Thm.transitive
(Thm.transitive
- (Thm.instantiate ([], [(vA, prem'), (vB, prem), (vC, concl)]) Drule.swap_prems_eq)
+ (Thm.instantiate (TVars.empty, Vars.make [(vA, prem'), (vB, prem), (vC, concl)])
+ Drule.swap_prems_eq)
eq')
- (Thm.instantiate ([], [(vA, prem), (vB, prem''), (vC, concl)]) Drule.swap_prems_eq)
+ (Thm.instantiate (TVars.empty, Vars.make [(vA, prem), (vB, prem''), (vC, concl)])
+ Drule.swap_prems_eq)
end
end