# HG changeset patch
# User kuncar
# Date 1393351662 -3600
# Node ID 30312334445923310ad206107693d5efd310d360
# Parent  84f6ac9f6e41064534e41d7e61c653d9feff9464
simplify a proof due to 6c95a39348bd

diff -r 84f6ac9f6e41 -r 303123344459 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Tue Feb 25 19:07:40 2014 +0100
+++ b/src/HOL/Library/FSet.thy	Tue Feb 25 19:07:42 2014 +0100
@@ -186,9 +186,8 @@
 
 lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem .
 
-(* FIXME why is not invariant here unfolded ? *)
-lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
-unfolding invariant_def Set.bind_def by clarsimp metis
+lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer 
+by (simp add: Set.bind_def)
 
 lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp