src/HOL/Library/Old_Datatype.thy

--- a/src/HOL/Library/Old_Datatype.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -21,7 +21,7 @@
   morphisms Rep_Node Abs_Node
   unfolding Node_def by auto
 
-text\<open>Datatypes will be represented by sets of type @{text node}\<close>
+text\<open>Datatypes will be represented by sets of type \<open>node\<close>\<close>
 
 type_synonym 'a item        = "('a, unit) node set"
 type_synonym ('a, 'b) dtree = "('a, 'b) node set"