--- 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