# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271837327 -7200
# Node ID 0a857f662e4c72c30e38fae443da80fe35aeb1ef
# Parent  60b5c61d3de26d34b25fb576fb3b1e6dc4deeeea
removed a sorry

diff -r 60b5c61d3de2 -r 0a857f662e4c Nominal/FSet.thy
--- a/Nominal/FSet.thy	Tue Apr 20 18:24:50 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 10:08:47 2010 +0200
@@ -603,7 +603,7 @@
   have "fcard_raw l = 0" by fact
   then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
   then have z: "l = []" using no_memb_nil by auto
-  then have "r = []" sorry
+  then have "r = []" using `l \<approx> r` by simp
   then show ?case using z list_eq2_refl by simp
 next
   case (Suc m)