--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -9,7 +9,7 @@
 begin
 
 text \<open>
-  Since the types @{typ cnam}, \<open>vnam\<close>, and \<open>mname\<close> are 
+  Since the types \<^typ>\<open>cnam\<close>, \<open>vnam\<close>, and \<open>mname\<close> are 
   anonymous, we describe distinctness of names in the example by axioms:
 \<close>
 axiomatization list_nam test_nam :: cnam