--- a/Nominal/Nominal2_FCB.thy	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/Nominal2_FCB.thy	Thu Apr 19 13:57:17 2018 +0100
@@ -396,7 +396,7 @@
 done
 
 lemma Abs_lst1_fcb2':
-  fixes a b :: "'a::at"
+  fixes a b :: "'a::at_base"
     and x y :: "'b :: fs"
     and c::"'c :: fs"
   assumes e: "[[atom a]]lst. x = [[atom b]]lst. y"
@@ -411,4 +411,4 @@
 apply(simp_all add: fresh_star_def inv_f_f inj_on_def atom_eqvt)
 done
 
-end
\ No newline at end of file
+end