src/Doc/Implementation/Logic.thy

   @{define_ML Thm.assume: "cterm -> thm"} \\
   @{define_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   @{define_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
   @{define_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   @{define_ML Thm.implies_elim: "thm -> thm -> thm"} \\
-  @{define_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
+  @{define_ML Thm.generalize: "Symtab.set * Symtab.set -> int -> thm -> thm"} \\
   @{define_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   -> thm -> thm"} \\
   @{define_ML Thm.add_axiom: "Proof.context ->
   binding * term -> theory -> (string * thm) * theory"} \\
   @{define_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->

   \<^descr> \<^ML>\<open>Thm.assume\<close>, \<^ML>\<open>Thm.forall_intr\<close>, \<^ML>\<open>Thm.forall_elim\<close>, \<^ML>\<open>Thm.implies_intr\<close>, and \<^ML>\<open>Thm.implies_elim\<close> correspond to the primitive
   inferences of \figref{fig:prim-rules}.
 
   \<^descr> \<^ML>\<open>Thm.generalize\<close>~\<open>(\<^vec>\<alpha>, \<^vec>x)\<close> corresponds to the
   \<open>generalize\<close> rules of \figref{fig:subst-rules}. Here collections of type and
-  term variables are generalized simultaneously, specified by the given basic
-  names.
+  term variables are generalized simultaneously, specified by the given sets of
+  basic names.
 
   \<^descr> \<^ML>\<open>Thm.instantiate\<close>~\<open>(\<^vec>\<alpha>\<^sub>s, \<^vec>x\<^sub>\<tau>)\<close> corresponds to the
   \<open>instantiate\<close> rules of \figref{fig:subst-rules}. Type variables are
   substituted before term variables. Note that the types in \<open>\<^vec>x\<^sub>\<tau>\<close> refer
   to the instantiated versions.