# HG changeset patch
# User wenzelm
# Date 1165777748 -3600
# Node ID 78248dda3a9009fb7d29c96fbe2a0245d266517b
# Parent  f4b20360751fc1f9f874b3bd54801e929922e6fc
fixed term_of_list;

diff -r f4b20360751f -r 78248dda3a90 src/HOL/List.thy
--- 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