--- a/Nominal/FSet.thy	Sun Jul 18 17:03:05 2010 +0100
+++ b/Nominal/FSet.thy	Sun Jul 18 19:07:05 2010 +0100
@@ -1328,6 +1328,7 @@
 apply(lifting_setup concat.simps(1))
 apply(rule test)
 apply(tactic {* resolve_tac (Quotient_Info.equiv_rules_get @{context}) 1 *})
+
 sorry
 
 lemma fconcat_insert: