--- a/src/Doc/Datatypes/Datatypes.thy Mon Feb 03 17:18:38 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Feb 03 17:55:50 2014 +0100
@@ -1103,7 +1103,7 @@
Pattern matching is only available for the argument on which the recursion takes
place. Fortunately, it is easy to generate pattern-maching equations using the
\keyw{simps\_of\_case} command provided by the theory
-\verb|~~/src/HOL/Library/Simps_Case_Conv|.
+\verb|~~/src/HOL/|\allowbreak\verb|Library/|\allowbreak\verb|Simps_Case_Conv|.
*}
simps_of_case at_simps: at.simps