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