src/Pure/drule.ML

   val strip_imp_concl: cterm -> cterm
   val cprems_of: thm -> cterm list
   val cterm_fun: (term -> term) -> (cterm -> cterm)
   val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
   val forall_intr_list: cterm list -> thm -> thm
-  val forall_intr_frees: thm -> thm
   val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
   val gen_all: thm -> thm
   val lift_all: cterm -> thm -> thm
   val legacy_freeze_thaw: thm -> thm * (thm -> thm)

     (Thm.fold_terms Term.add_tvars th []) th;
 
 (*Generalization over a list of variables*)
 val forall_intr_list = fold_rev forall_intr;
 
-(*Generalization over all suitable Free variables*)
-fun forall_intr_frees th =
-    let
-      val thy = Thm.theory_of_thm th;
-      val {prop, hyps, tpairs, ...} = rep_thm th;
-      val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
-      val frees = Term.fold_aterms (fn Free v =>
-        if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
-    in fold (forall_intr o cterm_of thy o Free) frees th end;
-
 (*Generalization over Vars -- canonical order*)
 fun forall_intr_vars th =
   fold forall_intr
     (map (Thm.cterm_of (Thm.theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th [])) th;
 

 
 (* old-style export without context *)
 
 val export_without_context_open =
   implies_intr_hyps
-  #> forall_intr_frees
+  #> Thm.forall_intr_frees
   #> `Thm.maxidx_of
   #-> (fn maxidx =>
     Thm.forall_elim_vars (maxidx + 1)
     #> Thm.strip_shyps
     #> zero_var_indexes