--- a/src/ZF/Constructible/Internalize.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Constructible/Internalize.thy Mon Dec 07 10:23:50 2015 +0100
@@ -634,7 +634,7 @@
text\<open>The additional variable in the premise, namely @{term f'}, is essential.
It lets @{term MH} depend upon @{term x}, which seems often necessary.
-The same thing occurs in @{text is_wfrec_reflection}.\<close>
+The same thing occurs in \<open>is_wfrec_reflection\<close>.\<close>
theorem is_recfun_reflection:
assumes MH_reflection:
"!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),