# HG changeset patch
# User wenzelm
# Date 952949954 -3600
# Node ID e5f8ee756a8a40f6887811a2a34d494db759b856
# Parent  dbd897e0d80475a6d238c2a0601184b5cf8ce72a
export vars_of;

diff -r dbd897e0d804 -r e5f8ee756a8a src/HOL/Tools/induct_method.ML
--- 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