src/HOL/Tools/datatype_package.ML
changeset 18377 0e1d025d57b3
parent 18319 c52b139ebde0
child 18418 bf448d999b7e
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Dec 08 20:16:17 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Dec 09 09:06:45 2005 +0100
     1.3 @@ -286,7 +286,7 @@
     1.4        
     1.5  fun add_rules simps case_thms size_thms rec_thms inject distinct
     1.6                    weak_case_congs cong_att =
     1.7 -  (#1 o PureThy.add_thmss [(("simps", simps), []),
     1.8 +  (snd o PureThy.add_thmss [(("simps", simps), []),
     1.9      (("", List.concat case_thms @ size_thms @ 
    1.10            List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
    1.11      (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
    1.12 @@ -313,7 +313,7 @@
    1.13      fun unnamed_rule i =
    1.14        (("", proj i induction), [InductAttrib.induct_type_global ""]);
    1.15      val rules = List.concat (map named_rules infos) @ map unnamed_rule (length infos upto n - 1);
    1.16 -  in #1 o PureThy.add_thms rules end;
    1.17 +  in snd o PureThy.add_thms rules end;
    1.18  
    1.19  
    1.20  
    1.21 @@ -533,11 +533,12 @@
    1.22  fun add_and_get_axioms_atts label tnames attss ts thy =
    1.23    foldr (fn (((tname, atts), t), (thy', axs)) =>
    1.24      let
    1.25 -      val (thy'', [ax]) = thy' |>
    1.26 -        Theory.add_path tname |>
    1.27 -        PureThy.add_axioms_i [((label, t), atts)];
    1.28 +      val ([ax], thy'') =
    1.29 +        thy'
    1.30 +        |> Theory.add_path tname
    1.31 +        |> PureThy.add_axioms_i [((label, t), atts)];
    1.32      in (Theory.parent_path thy'', ax::axs)
    1.33 -    end) (thy, []) (tnames ~~ attss ~~ ts);
    1.34 +    end) (thy, []) (tnames ~~ attss ~~ ts) |> swap;
    1.35  
    1.36  fun add_and_get_axioms label tnames =
    1.37    add_and_get_axioms_atts label tnames (replicate (length tnames) []);
    1.38 @@ -545,11 +546,12 @@
    1.39  fun add_and_get_axiomss label tnames tss thy =
    1.40    foldr (fn ((tname, ts), (thy', axss)) =>
    1.41      let
    1.42 -      val (thy'', [axs]) = thy' |>
    1.43 -        Theory.add_path tname |>
    1.44 -        PureThy.add_axiomss_i [((label, ts), [])];
    1.45 +      val ([axs], thy'') =
    1.46 +        thy'
    1.47 +        |> Theory.add_path tname
    1.48 +        |> PureThy.add_axiomss_i [((label, ts), [])];
    1.49      in (Theory.parent_path thy'', axs::axss)
    1.50 -    end) (thy, []) (tnames ~~ tss);
    1.51 +    end) (thy, []) (tnames ~~ tss) |> swap;
    1.52  
    1.53  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    1.54      case_names_induct case_names_exhausts thy =
    1.55 @@ -639,35 +641,35 @@
    1.56      val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
    1.57      val size_axs = if no_size then [] else DatatypeProp.make_size descr sorts thy2;
    1.58  
    1.59 -    val (thy3, (([induct], [rec_thms]), inject)) =
    1.60 -      thy2 |>
    1.61 -      Theory.add_path (space_implode "_" new_type_names) |>
    1.62 -      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
    1.63 -        [case_names_induct])] |>>>
    1.64 -      PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
    1.65 -      (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
    1.66 -      Theory.parent_path |>>>
    1.67 -      add_and_get_axiomss "inject" new_type_names
    1.68 -        (DatatypeProp.make_injs descr sorts);
    1.69 +    val ((([induct], [rec_thms]), inject), thy3) =
    1.70 +      thy2
    1.71 +      |> Theory.add_path (space_implode "_" new_type_names)
    1.72 +      |> PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
    1.73 +          [case_names_induct])]
    1.74 +      ||>> PureThy.add_axiomss_i [(("recs", rec_axs), [])]
    1.75 +      ||> (if no_size then I else snd o PureThy.add_axiomss_i [(("size", size_axs), [])])
    1.76 +      ||> Theory.parent_path
    1.77 +      ||>> add_and_get_axiomss "inject" new_type_names
    1.78 +            (DatatypeProp.make_injs descr sorts);
    1.79      val size_thms = if no_size then [] else get_thms thy3 (Name "size");
    1.80 -    val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
    1.81 +    val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names
    1.82        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
    1.83  
    1.84      val exhaust_ts = DatatypeProp.make_casedists descr sorts;
    1.85 -    val (thy5, exhaustion) = add_and_get_axioms_atts "exhaust" new_type_names
    1.86 +    val (exhaustion, thy5) = add_and_get_axioms_atts "exhaust" new_type_names
    1.87        (map Library.single case_names_exhausts) exhaust_ts thy4;
    1.88 -    val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
    1.89 +    val (case_thms, thy6) = add_and_get_axiomss "cases" new_type_names
    1.90        (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
    1.91      val (split_ts, split_asm_ts) = ListPair.unzip
    1.92        (DatatypeProp.make_splits new_type_names descr sorts thy6);
    1.93 -    val (thy7, split) = add_and_get_axioms "split" new_type_names split_ts thy6;
    1.94 -    val (thy8, split_asm) = add_and_get_axioms "split_asm" new_type_names
    1.95 +    val (split, thy7) = add_and_get_axioms "split" new_type_names split_ts thy6;
    1.96 +    val (split_asm, thy8) = add_and_get_axioms "split_asm" new_type_names
    1.97        split_asm_ts thy7;
    1.98 -    val (thy9, nchotomys) = add_and_get_axioms "nchotomy" new_type_names
    1.99 +    val (nchotomys, thy9) = add_and_get_axioms "nchotomy" new_type_names
   1.100        (DatatypeProp.make_nchotomys descr sorts) thy8;
   1.101 -    val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
   1.102 +    val (case_congs, thy10) = add_and_get_axioms "case_cong" new_type_names
   1.103        (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
   1.104 -    val (thy11, weak_case_congs) = add_and_get_axioms "weak_case_cong" new_type_names
   1.105 +    val (weak_case_congs, thy11) = add_and_get_axioms "weak_case_cong" new_type_names
   1.106        (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
   1.107  
   1.108      val dt_infos = map (make_dt_info descr' sorts induct reccomb_names' rec_thms)
   1.109 @@ -831,11 +833,12 @@
   1.110            [descr] sorts reccomb_names rec_thms thy8
   1.111        else ([], thy8);
   1.112  
   1.113 -    val ([induction'], thy10) = thy9 |>
   1.114 -      store_thmss "inject" new_type_names inject |> snd |>
   1.115 -      store_thmss "distinct" new_type_names distinct |> snd |>
   1.116 -      Theory.add_path (space_implode "_" new_type_names) |>
   1.117 -      PureThy.add_thms [(("induct", induction), [case_names_induct])] |> Library.swap;
   1.118 +    val ((_, [induction']), thy10) =
   1.119 +      thy9
   1.120 +      |> store_thmss "inject" new_type_names inject
   1.121 +      ||>> store_thmss "distinct" new_type_names distinct
   1.122 +      ||> Theory.add_path (space_implode "_" new_type_names)
   1.123 +      ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
   1.124  
   1.125      val dt_infos = map (make_dt_info descr sorts induction' reccomb_names rec_thms)
   1.126        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~