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