diff -r 2a803a1556d5 -r ca9eae5bd871 FSet.thy --- 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 \ 'a) \ 'a list \ 'a list"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd + make_const_def @{binding fmap} @{term "map::('a \ 'a) \ 'a list \ '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"},