src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33317 b4534348b8fd
parent 33278 ba9f52f56356
child 33338 de76079f973a
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 16:59:12 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 17:58:26 2009 +0100
     1.3 @@ -292,7 +292,7 @@
     1.4      val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
     1.5        let
     1.6          val Ts = map (typ_of_dtyp descr' sorts) cargs;
     1.7 -        val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
     1.8 +        val Ts' = map mk_dummyT (filter is_rec_type cargs)
     1.9        in Const (@{const_name undefined}, Ts @ Ts' ---> T')
    1.10        end) constrs) descr';
    1.11  
    1.12 @@ -305,7 +305,7 @@
    1.13            val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
    1.14              let
    1.15                val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.16 -              val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs);
    1.17 +              val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
    1.18                val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
    1.19                val frees = Library.take (length cargs, frees');
    1.20                val free = mk_Free "f" (Ts ---> T') j