src/Pure/proofterm.ML

   val forall_intr_proof': term -> proof -> proof
   val varify_proof: term -> (string * sort) list -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
-  val generalize_proof: string list * string list -> int -> term -> proof -> proof
+  val generalize_proof: Symtab.set * Symtab.set -> int -> term -> proof -> proof
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     -> proof -> proof
   val lift_proof: term -> int -> term -> proof -> proof
   val incr_indexes: int -> proof -> proof
   val assumption_proof: term list -> term -> int -> proof -> proof

 (* generalization *)
 
 fun generalize_proof (tfrees, frees) idx prop prf =
   let
     val gen =
-      if null frees then []
+      if Symtab.is_empty frees then []
       else
-        fold_aterms (fn Free (x, T) => member (op =) frees x ? insert (op =) (x, T) | _ => I)
-          (Term_Subst.generalize (tfrees, []) idx prop) [];
+        fold_aterms (fn Free (x, T) => Symtab.defined frees x ? insert (op =) (x, T) | _ => I)
+          (Term_Subst.generalize (tfrees, Symtab.empty) idx prop) [];
   in
     prf
     |> Same.commit (map_proof_terms_same
-        (Term_Subst.generalize_same (tfrees, []) idx)
+        (Term_Subst.generalize_same (tfrees, Symtab.empty) idx)
         (Term_Subst.generalizeT_same tfrees idx))
     |> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen
     |> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen
   end;