--- a/Nominal/Lift.thy	Sat May 01 09:15:46 2010 +0100
+++ b/Nominal/Lift.thy	Sun May 02 14:06:26 2010 +0100
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Abs" "Perm" "Equivp" "Rsp"
+        "Abs" "Perm" "Equivp" "Rsp" "Attic/Fv"
 begin
 
 
@@ -66,6 +66,9 @@
 end
 *}
 
+
+
+
 ML {*
 fun define_fv_alpha_export dt binds bns ctxt =
 let