tuned;

--- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Jul 11 09:57:20 2016 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Jul 11 10:43:27 2016 +0200
@@ -215,10 +215,8 @@
 begin
 
 sublocale Sum_any: comm_monoid_fun plus 0
-defines
-  Sum_any = Sum_any.G
-rewrites
-  "comm_monoid_set.F plus 0 = setsum"
+  defines Sum_any = Sum_any.G
+  rewrites "comm_monoid_set.F plus 0 = setsum"
 proof -
   show "comm_monoid_fun plus 0" ..
   then interpret Sum_any: comm_monoid_fun plus 0 .
@@ -284,10 +282,8 @@
 begin
 
 sublocale Prod_any: comm_monoid_fun times 1
-defines
-  Prod_any = Prod_any.G
-rewrites
-  "comm_monoid_set.F times 1 = setprod"
+  defines Prod_any = Prod_any.G
+  rewrites "comm_monoid_set.F times 1 = setprod"
 proof -
   show "comm_monoid_fun times 1" ..
   then interpret Prod_any: comm_monoid_fun times 1 .

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

--- a/src/HOL/Library/Polynomial.thy	Mon Jul 11 09:57:20 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy	Mon Jul 11 10:43:27 2016 +0200
@@ -55,7 +55,8 @@
 subsection \<open>Definition of type \<open>poly\<close>\<close>
 
 typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
-  morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
+  morphisms coeff Abs_poly
+  by (auto intro!: ALL_MOST)
 
 setup_lifting type_definition_poly
 

--- a/src/HOL/Library/Saturated.thy	Mon Jul 11 09:57:20 2016 +0200
+++ b/src/HOL/Library/Saturated.thy	Mon Jul 11 10:43:27 2016 +0200
@@ -215,8 +215,7 @@
 end
 
 interpretation Inf_sat: semilattice_neutr_set min "top :: 'a::len sat"
-rewrites
-  "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
+  rewrites "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
 proof -
   show "semilattice_neutr_set min (top :: 'a sat)"
     by standard (simp add: min_def)
@@ -225,8 +224,7 @@
 qed
 
 interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a::len sat"
-rewrites
-  "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
+  rewrites "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
 proof -
   show "semilattice_neutr_set max (bot :: 'a sat)"
     by standard (simp add: max_def bot.extremum_unique)