--- a/Nominal/Atoms.thy	Thu Oct 04 12:44:43 2012 +0100
+++ b/Nominal/Atoms.thy	Fri Oct 19 09:40:24 2012 +0100
@@ -42,7 +42,7 @@
 
 section {* Manual instantiation of class @{text at}. *}
 
-typedef (open) name = "{a. sort_of a = Sort ''name'' []}"
+typedef name = "{a. sort_of a = Sort ''name'' []}"
 by (rule exists_eq_simple_sort)
 
 instantiation name :: at
@@ -143,7 +143,7 @@
 
 declare sort_of_ty.simps [simp del]
 
-typedef (open) var = "{a. sort_of a \<in> range sort_of_ty}"
+typedef var = "{a. sort_of a \<in> range sort_of_ty}"
   by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp)
 
 instantiation var :: at_base