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