--- a/Nominal/Nominal2_Base.thy	Fri Dec 31 15:37:04 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Jan 03 16:19:27 2011 +0000
@@ -5,7 +5,8 @@
     Nominal Isabelle. 
 *)
 theory Nominal2_Base
-imports Main Infinite_Set
+imports Main 
+        "~~/src/HOL/Library/Infinite_Set"
         "~~/src/HOL/Quotient_Examples/FSet"
 uses ("nominal_library.ML")
      ("nominal_atoms.ML")
@@ -687,6 +688,7 @@
 instance bool :: pure
 proof qed (rule permute_bool_def)
 
+
 text {* Other type constructors preserve purity. *}
 
 instance "fun" :: (pure, pure) pure