--- a/Nominal/Nominal2_Atoms.thy	Sun Mar 07 21:30:57 2010 +0100
+++ b/Nominal/Nominal2_Atoms.thy	Mon Mar 08 15:01:01 2010 +0100
@@ -140,12 +140,13 @@
 
 subsection {* Syntax for coercing at-elements to the atom-type *}
 
+(*
 syntax
   "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)
 
 translations
   "_atom_constrain a t" => "atom (_constrain a t)"
-
+*)
 
 subsection {* A lemma for proving instances of class @{text at}. *}