--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 14 13:21:38 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Wed Apr 14 14:41:54 2010 +0200
@@ -6,6 +6,7 @@
 *)
 theory Nominal2_Base
 imports Main Infinite_Set
+uses ("nominal_library.ML")
 begin
 
 section {* Atoms and Sorts *}
@@ -1059,4 +1060,7 @@
     by auto
 qed
 
+(* nominal infrastructure *)
+use "nominal_library.ML"
+
 end