src/ZF/Tools/datatype_package.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18688 abf0f018b5ec
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -394,13 +394,14 @@
     1.4      val dom_sum =
     1.5        if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
     1.6        else read_i sdom;
     1.7 -
     1.8 -    val (thy', ((monos, type_intrs), type_elims)) = thy
     1.9 -      |> IsarThy.apply_theorems raw_monos
    1.10 -      |>>> IsarThy.apply_theorems raw_type_intrs
    1.11 -      |>>> IsarThy.apply_theorems raw_type_elims;
    1.12 -  in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy' end;
    1.13 -
    1.14 +  in
    1.15 +    thy
    1.16 +    |> IsarThy.apply_theorems raw_monos
    1.17 +    ||>> IsarThy.apply_theorems raw_type_intrs
    1.18 +    ||>> IsarThy.apply_theorems raw_type_elims
    1.19 +    |-> (fn ((monos, type_intrs), type_elims) =>
    1.20 +          add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims))
    1.21 +  end;
    1.22  
    1.23  (* outer syntax *)
    1.24