--- a/Nominal-General/Nominal2_Atoms.thy	Tue Apr 06 23:33:40 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy	Wed Apr 07 17:37:29 2010 +0200
@@ -242,6 +242,11 @@
 setup {* Sign.add_const_constraint
   (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
 
+ML {*
+  Theory_Target.instantiation;
+  Local_Theory.exit_global
+*}
+
 
 section {* Automation for creating concrete atom types *}
 
@@ -250,6 +255,4 @@
 use "nominal_atoms.ML"
 
 
-
-
 end