src/ZF/Tools/induct_tacs.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18688 abf0f018b5ec
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -172,16 +172,14 @@
     1.4    end;
     1.5  
     1.6  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
     1.7 -  let
     1.8 -    val (thy', (((elims, inducts), case_eqns), recursor_eqns)) = thy
     1.9 -      |> IsarThy.apply_theorems [raw_elim]
    1.10 -      |>>> IsarThy.apply_theorems [raw_induct]
    1.11 -      |>>> IsarThy.apply_theorems raw_case_eqns
    1.12 -      |>>> IsarThy.apply_theorems raw_recursor_eqns;
    1.13 -  in
    1.14 -    thy' |> rep_datatype_i (PureThy.single_thm "elimination" elims)
    1.15 -      (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns
    1.16 -  end;
    1.17 +  thy
    1.18 +  |> IsarThy.apply_theorems [raw_elim]
    1.19 +  ||>> IsarThy.apply_theorems [raw_induct]
    1.20 +  ||>> IsarThy.apply_theorems raw_case_eqns
    1.21 +  ||>> IsarThy.apply_theorems raw_recursor_eqns
    1.22 +  |-> (fn (((elims, inducts), case_eqns), recursor_eqns) =>
    1.23 +          rep_datatype_i (PureThy.single_thm "elimination" elims)
    1.24 +            (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns);
    1.25  
    1.26  
    1.27  (* theory setup *)