--- a/src/HOL/Library/code_lazy.ML Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Library/code_lazy.ML Sat Jan 05 17:24:33 2019 +0100
@@ -378,7 +378,7 @@
||>> 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 Unity}))
+ (#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]
val (Lazy_delay_thm, lthy8a) = mk_thm
((Lazy_delay_eq_name, mk_Lazy_delay_eq), [#thm lazy_ctr_def, @{thm force_delay}])