--- a/FSet.thy Tue Oct 27 14:46:38 2009 +0100
+++ b/FSet.thy Wed Oct 28 01:48:45 2009 +0100
@@ -168,7 +168,8 @@
thm fold_def
local_setup {*
- make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+ make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn
+ @{typ "'a list"} @{typ "'a fset"} #> snd
*}
term map
@@ -176,6 +177,8 @@
thm fmap_def
+
+
ML {*
val consts = [@{const_name "Nil"}, @{const_name "Cons"},
@{const_name "membship"}, @{const_name "card1"},