src/Pure/drule.ML
changeset 74200 17090e27aae9
parent 70494 41108e3e9ca5
child 74220 c49134ee16c1
--- a/src/Pure/drule.ML	Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Pure/drule.ML	Thu Aug 26 14:45:19 2021 +0200
@@ -52,7 +52,7 @@
 sig
   include BASIC_DRULE
   val outer_params: term -> (string * typ) list
-  val generalize: string list * string list -> thm -> thm
+  val generalize: Symtab.set * Symtab.set -> thm -> thm
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
   val beta_conv: cterm -> cterm -> cterm