diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Quickcheck_Random.thy
--- a/src/HOL/Quickcheck_Random.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Quickcheck_Random.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -127,7 +127,7 @@
 
 subsection \<open>Complex generators\<close>
 
-text \<open>Towards @{typ "'a \<Rightarrow> 'b"}\<close>
+text \<open>Towards \<^typ>\<open>'a \<Rightarrow> 'b\<close>\<close>
 
 axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
@@ -217,7 +217,7 @@
 
 code_printing
   constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun"
-  \<comment> \<open>With enough criminal energy this can be abused to derive @{prop False};
+  \<comment> \<open>With enough criminal energy this can be abused to derive \<^prop>\<open>False\<close>;
   for this reason we use a distinguished target \<open>Quickcheck\<close>
   not spoiling the regular trusted code generation\<close>