diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -177,7 +177,7 @@
 
 section \<open>Alternative list definitions\<close>
 
-subsection \<open>Alternative rules for @{text length}\<close>
+subsection \<open>Alternative rules for \<open>length\<close>\<close>
 
 definition size_list' :: "'a list => nat"
 where "size_list' = size"
@@ -191,7 +191,7 @@
 declare size_list'_def[symmetric, code_pred_inline]
 
 
-subsection \<open>Alternative rules for @{text list_all2}\<close>
+subsection \<open>Alternative rules for \<open>list_all2\<close>\<close>
 
 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
 by auto