--- a/src/HOL/Library/cconv.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Library/cconv.ML Fri Sep 10 14:59:19 2021 +0200
@@ -183,7 +183,8 @@
((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
| _ => cv ct)
-fun inst_imp_cong ct = Thm.instantiate ([], [((("A", 0), propT), ct)]) Drule.imp_cong
+fun inst_imp_cong ct =
+ Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), ct)]) Drule.imp_cong
(*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
fun concl_cconv 0 cv ct = cv ct
@@ -203,10 +204,12 @@
NONE => (As, B)
| SOME (A,B) => strip_prems (i - 1) (A::As) B
val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n []
- val rewr_imp_concl = Thm.instantiate ([], [((("C", 0), propT), concl)]) @{thm rewr_imp}
+ val rewr_imp_concl =
+ Thm.instantiate (TVars.empty, Vars.make [((("C", 0), propT), concl)]) @{thm rewr_imp}
val th1 = cv prem RS rewr_imp_concl
val nprems = Thm.nprems_of th1
- fun inst_cut_rl ct = Thm.instantiate ([], [((("psi", 0), propT), ct)]) cut_rl
+ fun inst_cut_rl ct =
+ Thm.instantiate (TVars.empty, Vars.make [((("psi", 0), propT), ct)]) cut_rl
fun f p th = (th RS inst_cut_rl p)
|> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq}))
in fold f prems th1 end