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