get Library/Permutations.thy compiled and working again

--- a/src/HOL/Library/Library.thy	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/HOL/Library/Library.thy	Tue Aug 16 07:06:54 2011 -0700
@@ -43,6 +43,7 @@
   OptionalSugar
   Option_ord
   Permutation
+  Permutations
   Poly_Deriv
   Polynomial
   Preorder

--- a/src/HOL/Library/Permutations.thy	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/HOL/Library/Permutations.thy	Tue Aug 16 07:06:54 2011 -0700
@@ -593,7 +593,8 @@
 
 lemma permutation_inverse_works: assumes p: "permutation p"
   shows "inv p o p = id" "p o inv p = id"
-using permutation_bijective[OF p] surj_iff bij_def inj_iff by auto
+  using permutation_bijective [OF p]
+  unfolding bij_def inj_iff surj_iff by auto
 
 lemma permutation_inverse_compose:
   assumes p: "permutation p" and q: "permutation q"