--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -75,7 +75,7 @@
     (thy : theory)
     : thm * theory =
   let
-    val i = Free ("i", natT)
+    val i = Free ("i", \<^Type>\<open>nat\<close>)
     val T = (fst o dest_cfunT o range_type o fastype_of) take_const
 
     val lub_take_eqn =