--- a/src/HOL/Tools/induct_method.ML Mon Mar 13 13:18:59 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML Mon Mar 13 13:19:14 2000 +0100
@@ -15,6 +15,7 @@
{type_cases: (string * thm) list, set_cases: (string * thm) list,
type_induct: (string * thm) list, set_induct: (string * thm) list}
val print_local_rules: Proof.context -> unit
+ val vars_of: term -> term list
val cases_type_global: string -> theory attribute
val cases_set_global: string -> theory attribute
val cases_type_local: string -> Proof.context attribute