# HG changeset patch
# User haftmann
# Date 1278082252 -7200
# Node ID f110a9fa87668fd849844e4d04e8bbd459ec276a
# Parent  e38abf437c2038a09fc2bbb28c692217890fab5b
tuned proof

diff -r e38abf437c20 -r f110a9fa8766 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Fri Jul 02 16:20:56 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Fri Jul 02 16:50:52 2010 +0200
@@ -18,7 +18,7 @@
 
 lemma Fset_member [simp]:
   "Fset (member A) = A"
-  by (rule member_inverse)
+  by (fact member_inverse)
 
 declare member_inject [simp]