--- a/Nominal-General/Nominal2_Atoms.thy	Wed Apr 07 17:37:29 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy	Wed Apr 07 22:08:46 2010 +0200
@@ -242,12 +242,6 @@
 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 *}
 
 text {* at the moment only single-sort concrete atoms are supported *}