diff -r 8d0294d877bd -r 107941e8fa01 src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Tue Sep 28 22:14:02 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML	Tue Sep 28 22:14:44 2021 +0200
@@ -378,8 +378,8 @@
       ||>> fold_map (mk_name ("case_" ^ short_type_name ^ "_lazy_") "") ctr_names
 
     val mk_Lazy_delay_eq =
-      (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ \<^const>\<open>Unity\<close>))
-      |> mk_eq |> all_abs [\<^typ>\<open>unit\<close> --> lazy_type]
+      (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ \<^Const>\<open>Unity\<close>))
+      |> mk_eq |> all_abs [\<^Type>\<open>unit\<close> --> lazy_type]
     val (Lazy_delay_thm, lthy8a) = mk_thm 
       ((Lazy_delay_eq_name, mk_Lazy_delay_eq), [#thm lazy_ctr_def, @{thm force_delay}])
       lthy8