src/HOL/Quickcheck_Exhaustive.thy
changeset 49948 744934b818c7
parent 48891 c0eafbd55de3
child 51126 df86080de4cb
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sat Oct 20 09:09:37 2012 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sat Oct 20 09:12:16 2012 +0200
     1.3 @@ -234,7 +234,7 @@
     1.4    "enum_term_of_fun = (%_ _. let
     1.5      enum_term_of_a = enum_term_of (TYPE('a));
     1.6      mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
     1.7 -  in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
     1.8 +  in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
     1.9   
    1.10  instance ..
    1.11  
    1.12 @@ -308,7 +308,7 @@
    1.13  definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
    1.14  where
    1.15    "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
    1.16 -     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
    1.17 +     (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
    1.18  
    1.19  instance ..
    1.20