diff -r 3b3089863eda -r 3a1b2d8c89aa src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Sun Apr 07 12:44:37 2019 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Sun Apr 07 08:26:57 2019 +0200
@@ -13,12 +13,16 @@
 imports
   Setup
   "HOL-Library.BNF_Axiomatization"
-  "HOL-Library.Cardinal_Notations"
   "HOL-Library.Countable"
   "HOL-Library.FSet"
   "HOL-Library.Simps_Case_Conv"
 begin
 
+
+(*<*)
+unbundle cardinal_syntax
+(*>*)
+
 section \<open>Introduction
   \label{sec:introduction}\<close>
 
@@ -2761,8 +2765,8 @@
 
 text \<open>
 The example below shows how to register a type as a BNF using the @{command bnf}
-command. Some of the proof obligations are best viewed with the theory
-\<^file>\<open>~~/src/HOL/Library/Cardinal_Notations.thy\<close> imported.
+command. Some of the proof obligations are best viewed with the bundle
+"cardinal_syntax" included.
 
 The type is simply a copy of the function space \<^typ>\<open>'d \<Rightarrow> 'a\<close>, where \<^typ>\<open>'a\<close>
 is live and \<^typ>\<open>'d\<close> is dead. We introduce it together with its map function,