src/HOL/Tools/datatype_package.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18451 5ff0244e25e8
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -766,13 +766,11 @@
     1.4    let
     1.5      val _ = Theory.requires thy0 "Inductive" "datatype representations";
     1.6  
     1.7 -    fun app_thmss srcs thy = foldl_map (fn (thy, x) => apply_theorems x thy) (thy, srcs);
     1.8 -    fun app_thm src thy = apsnd hd (apply_theorems [src] thy);
     1.9 -
    1.10 -    val (((thy1, induction), inject), distinct) = thy0
    1.11 -      |> app_thmss raw_distinct
    1.12 -      |> apfst (app_thmss raw_inject)
    1.13 -      |> apfst (apfst (app_thm raw_induction));
    1.14 +    val (((distinct, inject), [induction]), thy1) =
    1.15 +      thy0
    1.16 +      |> fold_map apply_theorems raw_distinct
    1.17 +      ||>> fold_map apply_theorems raw_inject
    1.18 +      ||>> apply_theorems [raw_induction];
    1.19      val sign = Theory.sign_of thy1;
    1.20  
    1.21      val induction' = freezeT induction;