--- 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

--- a/Nominal/Nominal2_Base.thy	Thu Oct 04 12:44:43 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Fri Oct 19 09:40:24 2012 +0100
@@ -80,10 +80,12 @@
 
 section {* Sort-Respecting Permutations *}
 
-typedef perm =
-  "{f. bij f \<and> finite {a. f a \<noteq> a} \<and> (\<forall>a. sort_of (f a) = sort_of a)}"
+definition
+  "perm \<equiv> {f. bij f \<and> finite {a. f a \<noteq> a} \<and> (\<forall>a. sort_of (f a) = sort_of a)}"
+
+typedef perm = "perm"
 proof
-  show "id \<in> ?perm" by simp
+  show "id \<in> perm" unfolding perm_def by simp
 qed
 
 lemma permI:

--- a/Nominal/nominal_atoms.ML	Thu Oct 04 12:44:43 2012 +0100
+++ b/Nominal/nominal_atoms.ML	Fri Oct 19 09:40:24 2012 +0100
@@ -35,7 +35,7 @@
     val set = atom_decl_set str;
     val tac = rtac @{thm exists_eq_simple_sort} 1;
     val ((full_tname, info  as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
-      Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
+      Typedef.add_typedef_global (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
     val newT = #abs_type (fst info);

--- a/Tutorial/Tutorial2s.thy	Thu Oct 04 12:44:43 2012 +0100
+++ b/Tutorial/Tutorial2s.thy	Fri Oct 19 09:40:24 2012 +0100
@@ -346,7 +346,8 @@
   moreover 
   have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto
   ultimately 
-  have "atom x \<sharp> Var x" using unbind_fake by auto
+  have "atom x \<sharp> Var x" 
+    by (rule_tac unbind_fake) (auto)
   then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base)
   then show "False" by simp
 qed