| changeset 21760 | 78248dda3a90 |
| parent 21754 | 6316163ae934 |
| child 21832 | 5a6f8514d0e9 |
--- a/src/HOL/List.thy Sun Dec 10 19:37:30 2006 +0100 +++ b/src/HOL/List.thy Sun Dec 10 20:09:08 2006 +0100 @@ -2526,7 +2526,7 @@ types_code "list" ("_ list") attach (term_of) {* -val term_of_list = HOLogic.mk_list; +fun term_of_list f T = HOLogic.mk_list T o map f; *} attach (test) {* fun gen_list' aG i j = frequency