--- a/src/Tools/induction.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/induction.ML Wed Oct 29 19:01:49 2014 +0100
@@ -3,7 +3,6 @@
val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
- val setup: theory -> theory
end
structure Induction: INDUCTION =
@@ -37,7 +36,7 @@
val induction_tac = Induct.gen_induct_tac (K name_hyps)
-val setup = Induct.gen_induct_setup @{binding induction} induction_tac
+val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
end