src/HOL/Tools/datatype_rep_proofs.ML
changeset 18377 0e1d025d57b3
parent 18358 0a733e11021a
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 08 20:16:17 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Dec 09 09:06:45 2005 +0100
     1.3 @@ -226,9 +226,10 @@
     1.4          val def_name = (Sign.base_name cname) ^ "_def";
     1.5          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
     1.6            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
     1.7 -        val ([def_thm], thy') = thy |>
     1.8 -          Theory.add_consts_i [(cname', constrT, mx)] |>
     1.9 -          (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
    1.10 +        val ([def_thm], thy') =
    1.11 +          thy
    1.12 +          |> Theory.add_consts_i [(cname', constrT, mx)]
    1.13 +          |> (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
    1.14  
    1.15        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
    1.16  
    1.17 @@ -639,10 +640,11 @@
    1.18              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
    1.19                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]));
    1.20  
    1.21 -    val (thy7, [dt_induct']) = thy6 |>
    1.22 -      Theory.add_path big_name |>
    1.23 -      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    1.24 -      Theory.parent_path;
    1.25 +    val ([dt_induct'], thy7) =
    1.26 +      thy6
    1.27 +      |> Theory.add_path big_name
    1.28 +      |> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])]
    1.29 +      ||> Theory.parent_path;
    1.30  
    1.31    in
    1.32      ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)