--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 28 08:22:20 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Wed Apr 28 08:24:46 2010 +0200
@@ -1102,6 +1102,11 @@
 
 section {* Concrete atoms types *}
 
+text {*
+  Class @{text at_base} allows types containing multiple sorts of atoms.
+  Class @{text at} only allows types with a single sort.
+*}
+
 class at_base = pt +
   fixes atom :: "'a \<Rightarrow> atom"
   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"