Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quickcheck_Exhaustive.thy
changeset 49948 744934b818c7
parent 48891 c0eafbd55de3
child 51126 df86080de4cb 
--- a/src/HOL/Quickcheck_Exhaustive.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -234,7 +234,7 @@
   "enum_term_of_fun = (%_ _. let
     enum_term_of_a = enum_term_of (TYPE('a));
     mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
-  in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
+  in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
  
 instance ..
 
@@ -308,7 +308,7 @@
 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
 where
   "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
-     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
+     (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
 
 instance ..
isabelle