--- a/src/Pure/drule.ML Mon Sep 06 12:11:17 2021 +0200
+++ b/src/Pure/drule.ML Mon Sep 06 12:23:06 2021 +0200
@@ -14,7 +14,6 @@
val strip_imp_concl: cterm -> cterm
val cprems_of: thm -> cterm list
val forall_intr_list: cterm list -> thm -> thm
- val forall_intr_vars: thm -> thm
val forall_elim_list: cterm list -> thm -> thm
val lift_all: Proof.context -> cterm -> thm -> thm
val implies_elim_list: thm -> thm list -> thm
@@ -164,11 +163,6 @@
(*Generalization over a list of variables*)
val forall_intr_list = fold_rev Thm.forall_intr;
-(*Generalization over Vars -- canonical order*)
-fun forall_intr_vars th =
- let val vs = build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Var (insert (op aconvc)))
- in fold Thm.forall_intr vs th end;
-
fun outer_params t =
let val vs = Term.strip_all_vars t
in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;