src/HOL/Tools/inductive.ML
changeset 44868 92be5b32ca71
parent 42491 4bb5de0aae66
child 45290 f599ac41e7f5
     1.1 --- a/src/HOL/Tools/inductive.ML	Sat Sep 10 10:29:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Sep 10 19:44:41 2011 +0200
     1.3 @@ -31,7 +31,6 @@
     1.4    val mono_del: attribute
     1.5    val get_monos: Proof.context -> thm list
     1.6    val mk_cases: Proof.context -> term -> thm
     1.7 -  val inductive_forall_name: string
     1.8    val inductive_forall_def: thm
     1.9    val rulify: thm -> thm
    1.10    val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
    1.11 @@ -92,7 +91,6 @@
    1.12  
    1.13  (** theory context references **)
    1.14  
    1.15 -val inductive_forall_name = "HOL.induct_forall";
    1.16  val inductive_forall_def = @{thm induct_forall_def};
    1.17  val inductive_conj_name = "HOL.induct_conj";
    1.18  val inductive_conj_def = @{thm induct_conj_def};