--- a/src/HOL/Algebra/abstract/Ring2.thy Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Sun May 15 17:45:53 2011 +0200
@@ -218,9 +218,9 @@
@{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}];
*} (* Note: r_one is not necessary in ring_ss *)
-method_setup ring =
- {* Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss))) *}
- {* computes distributive normal form in rings *}
+method_setup ring = {*
+ Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss)))
+*} "compute distributive normal form in rings"
subsection {* Rings and the summation operator *}