--- a/Nominal/Nominal2_FCB.thy	Mon Jan 16 12:42:47 2012 +0000
+++ b/Nominal/Nominal2_FCB.thy	Mon Jan 16 13:53:35 2012 +0000
@@ -301,19 +301,6 @@
   finally show ?thesis by simp
 qed
 
-typedef ('a::fs, 'b::fs) ffun = "{f::'a => 'b. finite (supp f)}"
-apply(subgoal_tac "\<exists>x::'b::fs. x \<in> (UNIV::('b::fs) set)")
-apply(erule exE)
-apply(rule_tac x="\<lambda>_. x" in exI)
-apply(auto)
-apply(rule_tac S="supp x" in supports_finite)
-apply(simp add: supports_def)
-apply(perm_simp)
-apply(simp add: fresh_def[symmetric])
-apply(simp add: swap_fresh_fresh)
-apply(simp add: finite_supp)
-done
-
 lemma Abs_lst_fcb2:
   fixes as bs :: "atom list"
     and x y :: "'b :: fs"