re-arranged tuples (theory * 'a) to ('a * theory) in Pure
authorhaftmann
Fri Dec 16 09:00:11 2005 +0100 (2005-12-16)
changeset 18418bf448d999b7e
parent 18417 149cc4126997
child 18419 30f4b1eda7cd
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/specification_package.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
src/Pure/axclass.ML
src/Pure/pure_thy.ML
src/Pure/thm.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -766,13 +766,11 @@
     1.4    let
     1.5      val _ = Theory.requires thy0 "Inductive" "datatype representations";
     1.6  
     1.7 -    fun app_thmss srcs thy = foldl_map (fn (thy, x) => apply_theorems x thy) (thy, srcs);
     1.8 -    fun app_thm src thy = apsnd hd (apply_theorems [src] thy);
     1.9 -
    1.10 -    val (((thy1, induction), inject), distinct) = thy0
    1.11 -      |> app_thmss raw_distinct
    1.12 -      |> apfst (app_thmss raw_inject)
    1.13 -      |> apfst (apfst (app_thm raw_induction));
    1.14 +    val (((distinct, inject), [induction]), thy1) =
    1.15 +      thy0
    1.16 +      |> fold_map apply_theorems raw_distinct
    1.17 +      ||>> fold_map apply_theorems raw_inject
    1.18 +      ||>> apply_theorems [raw_induction];
    1.19      val sign = Theory.sign_of thy1;
    1.20  
    1.21      val induction' = freezeT induction;
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Dec 15 21:51:31 2005 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 16 09:00:11 2005 +0100
     2.3 @@ -583,7 +583,7 @@
     2.4  
     2.5      val facts = args |> map (fn ((a, atts), props) =>
     2.6       ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
     2.7 -  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
     2.8 +  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
     2.9  
    2.10  val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
    2.11  val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
    2.12 @@ -864,7 +864,7 @@
    2.13      val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
    2.14      val (cs', intr_ts') = unify_consts thy cs intr_ts;
    2.15  
    2.16 -    val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
    2.17 +    val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos;
    2.18    in
    2.19      add_inductive_i verbose false "" coind false false cs'
    2.20        ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
     3.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Dec 15 21:51:31 2005 +0100
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Dec 16 09:00:11 2005 +0100
     3.3 @@ -272,7 +272,7 @@
     3.4      val _ = requires_recdef thy;
     3.5      val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
     3.6  
     3.7 -    val (thy1, congs) = thy |> app_thms raw_congs;
     3.8 +    val (congs, thy1) = thy |> app_thms raw_congs;
     3.9      val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;
    3.10      val ([induct_rules'], thy3) =
    3.11        thy2
     4.1 --- a/src/HOL/Tools/specification_package.ML	Thu Dec 15 21:51:31 2005 +0100
     4.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Dec 16 09:00:11 2005 +0100
     4.3 @@ -191,7 +191,6 @@
     4.4                          fun undo_imps thm =
     4.5                              equal_elim (symmetric rew_imp) thm
     4.6  
     4.7 -                        fun apply_atts arg = Thm.apply_attributes (arg, map (Attrib.global_attribute thy) atts)
     4.8                          fun add_final (arg as (thy, thm)) =
     4.9                              if name = ""
    4.10                              then arg |> Library.swap
    4.11 @@ -201,7 +200,7 @@
    4.12                          args |> apsnd (remove_alls frees)
    4.13                               |> apsnd undo_imps
    4.14                               |> apsnd standard
    4.15 -                             |> apply_atts
    4.16 +                             |> Thm.apply_attributes (map (Attrib.global_attribute thy) atts)
    4.17                               |> add_final
    4.18                               |> Library.swap
    4.19                      end
     5.1 --- a/src/Pure/Isar/attrib.ML	Thu Dec 15 21:51:31 2005 +0100
     5.2 +++ b/src/Pure/Isar/attrib.ML	Fri Dec 16 09:00:11 2005 +0100
     5.3 @@ -180,7 +180,7 @@
     5.4      let
     5.5        val ths = PureThy.select_thm thmref fact;
     5.6        val atts = map (attrib (theory_of st)) srcs;
     5.7 -      val (st', ths') = Thm.applys_attributes ((st, ths), atts);
     5.8 +      val (st', ths') = Thm.applys_attributes atts (st, ths);
     5.9      in (st', pick name ths') end));
    5.10  
    5.11  val global_thm = gen_thm I global_attribute_i PureThy.get_thms PureThy.single_thm;
     6.1 --- a/src/Pure/Isar/context_rules.ML	Thu Dec 15 21:51:31 2005 +0100
     6.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Dec 16 09:00:11 2005 +0100
     6.3 @@ -258,7 +258,7 @@
     6.4  (* low-level modifiers *)
     6.5  
     6.6  fun modifier att (x, ths) =
     6.7 -  #1 (Thm.applys_attributes ((x, rev ths), [att]));
     6.8 +  fst (Thm.applys_attributes [att] (x, rev ths));
     6.9  
    6.10  val addXIs_global = modifier (intro_query_global NONE);
    6.11  val addXEs_global = modifier (elim_query_global NONE);
     7.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Dec 15 21:51:31 2005 +0100
     7.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Dec 16 09:00:11 2005 +0100
     7.3 @@ -11,14 +11,14 @@
     7.4    val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
     7.5    val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
     7.6    val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
     7.7 -  val apply_theorems: (thmref * Attrib.src list) list -> theory -> theory * thm list
     7.8 -  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
     7.9 +  val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
    7.10 +  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> thm list * theory
    7.11    val theorems: string ->
    7.12      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    7.13 -    -> theory -> theory * (string * thm list) list
    7.14 +    -> theory -> (string * thm list) list * theory 
    7.15    val theorems_i: string ->
    7.16      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
    7.17 -    -> theory -> theory * (string * thm list) list
    7.18 +    -> theory -> (string * thm list) list * theory
    7.19    val smart_theorems: string -> xstring option ->
    7.20      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    7.21      theory -> theory * Proof.context
    7.22 @@ -75,21 +75,19 @@
    7.23  
    7.24  fun theorems kind args thy = thy
    7.25    |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args)
    7.26 -  |> tap (present_theorems kind)
    7.27 -  |> swap;
    7.28 +  |> tap (present_theorems kind);
    7.29  
    7.30  fun theorems_i kind args =
    7.31    PureThy.note_thmss_i (Drule.kind kind) args
    7.32 -  #> tap (present_theorems kind)
    7.33 -  #> swap;
    7.34 +  #> tap (present_theorems kind);
    7.35  
    7.36 -fun apply_theorems args = apsnd (List.concat o map snd) o theorems "" [(("", []), args)];
    7.37 -fun apply_theorems_i args = apsnd (List.concat o map snd) o theorems_i "" [(("", []), args)];
    7.38 +fun apply_theorems args = apfst (List.concat o map snd) o theorems "" [(("", []), args)];
    7.39 +fun apply_theorems_i args = apfst (List.concat o map snd) o theorems_i "" [(("", []), args)];
    7.40  
    7.41  fun smart_theorems kind NONE args thy = thy
    7.42        |> theorems kind args
    7.43 -      |> tap (present_theorems kind o swap)
    7.44 -      |> (fn (thy, _) => (thy, ProofContext.init thy))
    7.45 +      |> tap (present_theorems kind)
    7.46 +      |> (fn (_, thy) => (thy, ProofContext.init thy))
    7.47    | smart_theorems kind (SOME loc) args thy = thy
    7.48        |> Locale.note_thmss kind loc args
    7.49        |> tap (present_theorems kind o swap o apfst #1)
     8.1 --- a/src/Pure/Isar/method.ML	Thu Dec 15 21:51:31 2005 +0100
     8.2 +++ b/src/Pure/Isar/method.ML	Fri Dec 16 09:00:11 2005 +0100
     8.3 @@ -624,7 +624,7 @@
     8.4  fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
     8.5  fun thmss ss = Scan.repeat (thms ss) >> List.concat;
     8.6  
     8.7 -fun apply (f, att) (ctxt, ths) = Thm.applys_attributes ((f ctxt, ths), [att]);
     8.8 +fun apply (f, att) (ctxt, ths) = Thm.applys_attributes [att] (f ctxt, ths);
     8.9  
    8.10  fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt =>
    8.11    Scan.succeed (apply m (ctxt, ths)))) >> #2;
     9.1 --- a/src/Pure/Isar/proof_context.ML	Thu Dec 15 21:51:31 2005 +0100
     9.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Dec 16 09:00:11 2005 +0100
     9.3 @@ -1018,7 +1018,7 @@
     9.4  fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt =>
     9.5    let
     9.6      fun app (th, attrs) (ct, ths) =
     9.7 -      let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
     9.8 +      let val (ct', th') = Thm.applys_attributes (attrs @ more_attrs) (ct, get ctxt th)
     9.9        in (ct', th' :: ths) end;
    9.10      val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []);
    9.11      val thms = List.concat (rev rev_thms);
    10.1 --- a/src/Pure/axclass.ML	Thu Dec 15 21:51:31 2005 +0100
    10.2 +++ b/src/Pure/axclass.ML	Fri Dec 16 09:00:11 2005 +0100
    10.3 @@ -11,9 +11,9 @@
    10.4    val print_axclasses: theory -> unit
    10.5    val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
    10.6    val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
    10.7 -    theory -> theory * {intro: thm, axioms: thm list}
    10.8 +    theory -> {intro: thm, axioms: thm list} * theory
    10.9    val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list ->
   10.10 -    theory -> theory * {intro: thm, axioms: thm list}
   10.11 +    theory -> {intro: thm, axioms: thm list} * theory
   10.12    val add_classrel_thms: thm list -> theory -> theory
   10.13    val add_arity_thms: thm list -> theory -> theory
   10.14    val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
   10.15 @@ -210,7 +210,7 @@
   10.16        |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
   10.17        ||> Theory.restore_naming class_thy
   10.18        ||> AxclassesData.map (Symtab.update (class, info));
   10.19 -  in (final_thy, {intro = intro, axioms = axioms}) end;
   10.20 +  in ({intro = intro, axioms = axioms}, final_thy) end;
   10.21  
   10.22  in
   10.23  
   10.24 @@ -347,7 +347,7 @@
   10.25    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
   10.26      ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
   10.27          P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
   10.28 -      >> (Toplevel.theory o (#1 oo uncurry add_axclass)));
   10.29 +      >> (Toplevel.theory o (snd oo uncurry add_axclass)));
   10.30  
   10.31  val instanceP =
   10.32    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    11.1 --- a/src/Pure/pure_thy.ML	Thu Dec 15 21:51:31 2005 +0100
    11.2 +++ b/src/Pure/pure_thy.ML	Fri Dec 16 09:00:11 2005 +0100
    11.3 @@ -308,8 +308,8 @@
    11.4  fun name_thmss name xs =
    11.5    (case filter_out (null o fst) xs of
    11.6      [([x], z)] => [([name_thm true (name, x)], z)]
    11.7 -  | _ => snd (foldl_map (fn (i, (ys, z)) =>
    11.8 -    (i + length ys, (map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs)));
    11.9 +  | _ => fst (fold_map (fn (ys, z) => fn i =>
   11.10 +    ((map (name_thm true) (gen_names i (length ys) name ~~ ys), z), i + length ys)) xs 0));
   11.11  
   11.12  
   11.13  (* enter_thms *)
   11.14 @@ -317,7 +317,7 @@
   11.15  fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
   11.16  fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
   11.17  
   11.18 -fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms)
   11.19 +fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap
   11.20    | enter_thms pre_name post_name app_att (bname, thms) thy =
   11.21        let
   11.22          val name = Sign.full_name thy bname;
   11.23 @@ -333,15 +333,15 @@
   11.24              if Thm.eq_thms (thms', thms'') then warn_same name
   11.25              else warn_overwrite name);
   11.26          r := {theorems = (space', theorems'), index = index'};
   11.27 -        (thy', thms')
   11.28 +        (thms', thy')
   11.29        end;
   11.30  
   11.31  
   11.32  (* add_thms(s) *)
   11.33  
   11.34  fun add_thms_atts pre_name ((bname, thms), atts) =
   11.35 -  swap o enter_thms pre_name (name_thms false)
   11.36 -    (Thm.applys_attributes o rpair atts) (bname, thms);
   11.37 +  enter_thms pre_name (name_thms false)
   11.38 +    (Thm.applys_attributes atts) (bname, thms);
   11.39  
   11.40  fun gen_add_thmss pre_name =
   11.41    fold_map (add_thms_atts pre_name);
   11.42 @@ -357,21 +357,21 @@
   11.43  
   11.44  local
   11.45  
   11.46 -fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
   11.47 +fun gen_note_thss get kind_att ((bname, more_atts), ths_atts) thy =
   11.48    let
   11.49 -    fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
   11.50 -    val (thy', thms) = thy |> enter_thms
   11.51 +    fun app (x, (ths, atts)) = Thm.applys_attributes atts (x, ths);
   11.52 +    val (thms, thy') = thy |> enter_thms
   11.53        name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
   11.54        (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
   11.55 -  in (thy', (bname, thms)) end;
   11.56 +  in ((bname, thms), thy') end;
   11.57  
   11.58 -fun gen_note_thmss get kind_att args thy =
   11.59 -  foldl_map (gen_note_thss get kind_att) (thy, args);
   11.60 +fun gen_note_thmss get kind_att =
   11.61 +  fold_map (gen_note_thss get kind_att);
   11.62  
   11.63  in
   11.64  
   11.65 -val note_thmss = swap ooo gen_note_thmss get_thms;
   11.66 -val note_thmss_i = swap ooo gen_note_thmss (K I);
   11.67 +val note_thmss = gen_note_thmss get_thms;
   11.68 +val note_thmss_i = gen_note_thmss (K I);
   11.69  
   11.70  end;
   11.71  
   11.72 @@ -390,12 +390,12 @@
   11.73  fun smart_store _ (name, []) =
   11.74        error ("Cannot store empty list of theorems: " ^ quote name)
   11.75    | smart_store name_thm (name, [thm]) =
   11.76 -      #2 (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
   11.77 +      fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
   11.78    | smart_store name_thm (name, thms) =
   11.79        let
   11.80          fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th);
   11.81          val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms);
   11.82 -      in #2 (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
   11.83 +      in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
   11.84  
   11.85  in
   11.86  
    12.1 --- a/src/Pure/thm.ML	Thu Dec 15 21:51:31 2005 +0100
    12.2 +++ b/src/Pure/thm.ML	Fri Dec 16 09:00:11 2005 +0100
    12.3 @@ -142,8 +142,8 @@
    12.4    val no_prems: thm -> bool
    12.5    val no_attributes: 'a -> 'a * 'b list
    12.6    val simple_fact: 'a -> ('a * 'b list) list
    12.7 -  val apply_attributes: ('a * thm) * 'a attribute list -> 'a * thm
    12.8 -  val applys_attributes: ('a * thm list) * 'a attribute list -> 'a * thm list
    12.9 +  val apply_attributes: 'a attribute list -> 'a * thm -> 'a * thm
   12.10 +  val applys_attributes: 'a attribute list -> 'a * thm list -> 'a * thm list
   12.11    val terms_of_tpairs: (term * term) list -> term list
   12.12    val full_prop_of: thm -> term
   12.13    val get_name_tags: thm -> string * tag list
   12.14 @@ -400,8 +400,8 @@
   12.15  
   12.16  fun no_attributes x = (x, []);
   12.17  fun simple_fact x = [(x, [])];
   12.18 -fun apply_attributes (x_th, atts) = Library.apply atts x_th;
   12.19 -fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
   12.20 +val apply_attributes = Library.apply;
   12.21 +fun applys_attributes atts = foldl_map (Library.apply atts);
   12.22  
   12.23  
   12.24  (* hyps *)
    13.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Dec 15 21:51:31 2005 +0100
    13.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Dec 16 09:00:11 2005 +0100
    13.3 @@ -394,13 +394,14 @@
    13.4      val dom_sum =
    13.5        if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
    13.6        else read_i sdom;
    13.7 -
    13.8 -    val (thy', ((monos, type_intrs), type_elims)) = thy
    13.9 -      |> IsarThy.apply_theorems raw_monos
   13.10 -      |>>> IsarThy.apply_theorems raw_type_intrs
   13.11 -      |>>> IsarThy.apply_theorems raw_type_elims;
   13.12 -  in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy' end;
   13.13 -
   13.14 +  in
   13.15 +    thy
   13.16 +    |> IsarThy.apply_theorems raw_monos
   13.17 +    ||>> IsarThy.apply_theorems raw_type_intrs
   13.18 +    ||>> IsarThy.apply_theorems raw_type_elims
   13.19 +    |-> (fn ((monos, type_intrs), type_elims) =>
   13.20 +          add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims))
   13.21 +  end;
   13.22  
   13.23  (* outer syntax *)
   13.24  
    14.1 --- a/src/ZF/Tools/ind_cases.ML	Thu Dec 15 21:51:31 2005 +0100
    14.2 +++ b/src/ZF/Tools/ind_cases.ML	Fri Dec 16 09:00:11 2005 +0100
    14.3 @@ -55,7 +55,7 @@
    14.4      val facts = args |> map (fn ((name, srcs), props) =>
    14.5        ((name, map (Attrib.global_attribute thy) srcs),
    14.6          map (Thm.no_attributes o single o mk_cases) props));
    14.7 -  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
    14.8 +  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
    14.9  
   14.10  
   14.11  (* ind_cases method *)
    15.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Dec 15 21:51:31 2005 +0100
    15.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Dec 16 09:00:11 2005 +0100
    15.3 @@ -172,16 +172,14 @@
    15.4    end;
    15.5  
    15.6  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
    15.7 -  let
    15.8 -    val (thy', (((elims, inducts), case_eqns), recursor_eqns)) = thy
    15.9 -      |> IsarThy.apply_theorems [raw_elim]
   15.10 -      |>>> IsarThy.apply_theorems [raw_induct]
   15.11 -      |>>> IsarThy.apply_theorems raw_case_eqns
   15.12 -      |>>> IsarThy.apply_theorems raw_recursor_eqns;
   15.13 -  in
   15.14 -    thy' |> rep_datatype_i (PureThy.single_thm "elimination" elims)
   15.15 -      (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns
   15.16 -  end;
   15.17 +  thy
   15.18 +  |> IsarThy.apply_theorems [raw_elim]
   15.19 +  ||>> IsarThy.apply_theorems [raw_induct]
   15.20 +  ||>> IsarThy.apply_theorems raw_case_eqns
   15.21 +  ||>> IsarThy.apply_theorems raw_recursor_eqns
   15.22 +  |-> (fn (((elims, inducts), case_eqns), recursor_eqns) =>
   15.23 +          rep_datatype_i (PureThy.single_thm "elimination" elims)
   15.24 +            (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns);
   15.25  
   15.26  
   15.27  (* theory setup *)
    16.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Dec 15 21:51:31 2005 +0100
    16.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Dec 16 09:00:11 2005 +0100
    16.3 @@ -567,16 +567,16 @@
    16.4      val dom_sum = read Ind_Syntax.iT sdom_sum;
    16.5      val intr_tms = map (read propT o snd o fst) sintrs;
    16.6      val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs;
    16.7 -
    16.8 -    val (thy', (((monos, con_defs), type_intrs), type_elims)) = thy
    16.9 -      |> IsarThy.apply_theorems raw_monos
   16.10 -      |>>> IsarThy.apply_theorems raw_con_defs
   16.11 -      |>>> IsarThy.apply_theorems raw_type_intrs
   16.12 -      |>>> IsarThy.apply_theorems raw_type_elims;
   16.13    in
   16.14 -    add_inductive_i true (rec_tms, dom_sum) intr_specs
   16.15 -      (monos, con_defs, type_intrs, type_elims) thy'
   16.16 -  end
   16.17 +    thy
   16.18 +    |> IsarThy.apply_theorems raw_monos
   16.19 +    ||>> IsarThy.apply_theorems raw_con_defs
   16.20 +    ||>> IsarThy.apply_theorems raw_type_intrs
   16.21 +    ||>> IsarThy.apply_theorems raw_type_elims
   16.22 +    |-> (fn (((monos, con_defs), type_intrs), type_elims) =>
   16.23 +          add_inductive_i true (rec_tms, dom_sum) intr_specs
   16.24 +            (monos, con_defs, type_intrs, type_elims))
   16.25 +  end;
   16.26  
   16.27  
   16.28  (* outer syntax *)