src/HOL/Tools/inductive_package.ML
changeset 18377 0e1d025d57b3
parent 18358 0a733e11021a
child 18418 bf448d999b7e
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Dec 08 20:16:17 2005 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 09 09:06:45 2005 +0100
     1.3 @@ -451,13 +451,13 @@
     1.4      fun cases_spec name elim thy =
     1.5        thy
     1.6        |> Theory.add_path (Sign.base_name name)
     1.7 -      |> (fst o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
     1.8 +      |> (snd o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
     1.9        |> Theory.parent_path;
    1.10      val cases_specs = if no_elim then [] else map2 cases_spec names elims;
    1.11  
    1.12      val induct_att =
    1.13        if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global;
    1.14 -    fun induct_spec (name, th) = #1 o PureThy.add_thms
    1.15 +    fun induct_spec (name, th) = snd o PureThy.add_thms
    1.16        [(("", RuleCases.save induct th), [induct_att name])];
    1.17      val induct_specs =
    1.18        if no_induct then [] else map induct_spec (project_rules names induct);
    1.19 @@ -794,16 +794,17 @@
    1.20          (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
    1.21        else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]);
    1.22  
    1.23 -    val (thy2, intrs') =
    1.24 -      thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
    1.25 -    val (thy3, ([_, elims'], [induct'])) =
    1.26 +    val (intrs', thy2) =
    1.27 +      thy1
    1.28 +      |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
    1.29 +    val (([_, elims'], [induct']), thy3) =
    1.30        thy2
    1.31        |> PureThy.add_thmss
    1.32          [(("intros", intrs'), []),
    1.33            (("elims", elims), [RuleCases.consumes 1])]
    1.34 -      |>>> PureThy.add_thms
    1.35 +      ||>> PureThy.add_thms
    1.36          [((coind_prefix coind ^ "induct", rulify (#1 induct)), #2 induct)]
    1.37 -      |>> Theory.parent_path;
    1.38 +      ||> Theory.parent_path;
    1.39    in (thy3,
    1.40      {defs = fp_def :: rec_sets_defs,
    1.41       mono = mono,