diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Library/code_lazy.ML
--- 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}])