src/Tools/induction.ML
changeset 58826 2ed2eaabe3df
parent 56506 c1f04411d43f
child 59582 0fbed69ff081
     1.1 --- a/src/Tools/induction.ML	Wed Oct 29 17:01:44 2014 +0100
     1.2 +++ b/src/Tools/induction.ML	Wed Oct 29 19:01:49 2014 +0100
     1.3 @@ -3,7 +3,6 @@
     1.4    val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     1.5      (string * typ) list list -> term option list -> thm list option ->
     1.6      thm list -> int -> cases_tactic
     1.7 -  val setup: theory -> theory
     1.8  end
     1.9  
    1.10  structure Induction: INDUCTION =
    1.11 @@ -37,7 +36,7 @@
    1.12  
    1.13  val induction_tac = Induct.gen_induct_tac (K name_hyps)
    1.14  
    1.15 -val setup = Induct.gen_induct_setup @{binding induction} induction_tac
    1.16 +val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
    1.17  
    1.18  end
    1.19