src/HOL/Tools/inductive_package.ML
changeset 12876 a70df1e5bf10
parent 12798 f7e2d0d32ea7
child 12902 a23dc0b7566f
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Feb 12 20:25:58 2002 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Feb 12 20:28:27 2002 +0100
     1.3 @@ -44,10 +44,8 @@
     1.4    val inductive_forall_name: string
     1.5    val inductive_forall_def: thm
     1.6    val rulify: thm -> thm
     1.7 -  val inductive_cases: (((bstring * Args.src list) * string list) * Comment.text) list
     1.8 -    -> theory -> theory
     1.9 -  val inductive_cases_i: (((bstring * theory attribute list) * term list) * Comment.text) list
    1.10 -    -> theory -> theory
    1.11 +  val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
    1.12 +  val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
    1.13    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    1.14      ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
    1.15        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.16 @@ -587,8 +585,8 @@
    1.17      val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy);
    1.18      val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
    1.19  
    1.20 -    val facts = args |> map (fn (((a, atts), props), comment) =>
    1.21 -     (((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props), comment));
    1.22 +    val facts = args |> map (fn ((a, atts), props) =>
    1.23 +     ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
    1.24    in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
    1.25  
    1.26  val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
    1.27 @@ -874,10 +872,10 @@
    1.28    #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
    1.29  
    1.30  fun ind_decl coind =
    1.31 -  (Scan.repeat1 P.term --| P.marg_comment) --
    1.32 +  Scan.repeat1 P.term --
    1.33    (P.$$$ "intros" |--
    1.34 -    P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
    1.35 -  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) []
    1.36 +    P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
    1.37 +  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
    1.38    >> (Toplevel.theory o mk_ind coind);
    1.39  
    1.40  val inductiveP =
    1.41 @@ -888,7 +886,7 @@
    1.42  
    1.43  
    1.44  val ind_cases =
    1.45 -  P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment)
    1.46 +  P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
    1.47    >> (Toplevel.theory o inductive_cases);
    1.48  
    1.49  val inductive_casesP =