diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Thu May 26 17:51:22 2016 +0200
@@ -241,7 +241,7 @@
 regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class\<close>
 
 text\<open>This theorem is easily proved but never used. There's no obvious way
-even to state the analogous result, @{text FnCall_Cons}.\<close>
+even to state the analogous result, \<open>FnCall_Cons\<close>.\<close>
 lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})"
   by (simp add: FnCall_def)
 
@@ -390,7 +390,7 @@
 
 
 subsection\<open>The Abstract Discriminator\<close>
-text\<open>However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this
+text\<open>However, as \<open>FnCall_Var_neq_Var\<close> illustrates, we don't need this
 function in order to prove discrimination theorems.\<close>
 
 definition