src/HOL/Library/Perm.thy

--- a/src/HOL/Library/Perm.thy	Mon Jul 11 09:57:20 2016 +0200
+++ b/src/HOL/Library/Perm.thy	Mon Jul 11 10:43:27 2016 +0200
@@ -20,7 +20,9 @@
 
 typedef 'a perm = "{f :: 'a \<Rightarrow> 'a. bij f \<and> finite {a. f a \<noteq> a}}"
   morphisms "apply" Perm
-  by (rule exI [of _ id]) simp
+proof
+  show "id \<in> ?perm" by simp
+qed
 
 setup_lifting type_definition_perm