diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/code_lazy.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -84,10 +84,10 @@
   let
     val (name, _) = mk_name "lazy_" "" short_type_name lthy
     val freeT = HOLogic.unitT --> lazyT
-    val lazyT' = Type (@{type_name lazy}, [lazyT])
+    val lazyT' = Type (\<^type_name>\<open>lazy\<close>, [lazyT])
     val def = Logic.all_const freeT $ absdummy freeT (Logic.mk_equals (
       Free (name, (freeT --> eagerT)) $ Bound 0,
-      lazy_ctr $ (Const (@{const_name delay}, (freeT --> lazyT')) $ Bound 0)))
+      lazy_ctr $ (Const (\<^const_name>\<open>delay\<close>, (freeT --> lazyT')) $ Bound 0)))
     val (_, lthy') = Local_Theory.open_target lthy
     val ((t, (_, thm)), lthy') = Specification.definition NONE [] [] 
       ((Thm.def_binding (Binding.name name), []), def) lthy'
@@ -235,7 +235,7 @@
         val (result, lthy1) = (Typedef.add_typedef
             { overloaded=false }
             (binding, rev (Term.add_tfreesT eager_type []), Mixfix.NoSyn)
-            (Const (@{const_name "top"}, Type (@{type_name set}, [eager_type])))
+            (Const (\<^const_name>\<open>top\<close>, Type (\<^type_name>\<open>set\<close>, [eager_type])))
             NONE
             (fn ctxt => resolve_tac ctxt [@{thm UNIV_witness}] 1)
           o (Local_Theory.open_target #> snd)) lthy
@@ -270,9 +270,9 @@
       ctrs
 
     fun to_destr_eagerT typ = case typ of
-          Type (@{type_name "fun"}, [_, Type (@{type_name "fun"}, Ts)]) => 
-          to_destr_eagerT (Type (@{type_name "fun"}, Ts))
-        | Type (@{type_name "fun"}, [T, _]) => T
+          Type (\<^type_name>\<open>fun\<close>, [_, Type (\<^type_name>\<open>fun\<close>, Ts)]) => 
+          to_destr_eagerT (Type (\<^type_name>\<open>fun\<close>, Ts))
+        | Type (\<^type_name>\<open>fun\<close>, [T, _]) => T
         | _ => raise Match
     val (case', lthy4) = 
       let
@@ -299,7 +299,7 @@
         ({binding = binding, const = Const (Local_Theory.full_name lthy2 binding, T), thm = def_thm}, lthy2)
       end;
     
-    val lazy_datatype = Type (@{type_name lazy}, [lazy_type])
+    val lazy_datatype = Type (\<^type_name>\<open>lazy\<close>, [lazy_type])
     val Lazy_type = lazy_datatype --> eagerT
     val unstr_type = eagerT --> lazy_datatype
     
@@ -307,8 +307,8 @@
       if n > i then apply_bounds i (n-1) (term $ Bound (n-1))
       else term
     fun all_abs Ts t = Logic.list_all (map (pair Name.uu) Ts, t)
-    fun mk_force t = Const (@{const_name force}, lazy_datatype --> lazy_type) $ t
-    fun mk_delay t = Const (@{const_name delay}, (@{typ unit} --> lazy_type) --> lazy_datatype) $ t
+    fun mk_force t = Const (\<^const_name>\<open>force\<close>, lazy_datatype --> lazy_type) $ t
+    fun mk_delay t = Const (\<^const_name>\<open>delay\<close>, (\<^typ>\<open>unit\<close> --> lazy_type) --> lazy_datatype) $ t
 
     val lazy_ctr = all_abs [lazy_datatype]
       (Logic.mk_equals (Free (lazy_ctr_name, Lazy_type) $ Bound 0, Rep_lazy $ mk_force (Bound 0)))
@@ -316,13 +316,13 @@
 
     val lazy_sel = all_abs [eagerT]
       (Logic.mk_equals (Free (lazy_sel_name, unstr_type) $ Bound 0, 
-        mk_delay (Abs (Name.uu, @{typ unit}, Abs_lazy $ Bound 1))))
+        mk_delay (Abs (Name.uu, \<^typ>\<open>unit\<close>, Abs_lazy $ Bound 1))))
     val (lazy_sel_def, lthy6) = mk_def (lazy_sel_name, unstr_type, lazy_sel) lthy5
 
     fun mk_lazy_ctr (name, eager_ctr) =
       let
         val (_, ctrT) = dest_Const eager_ctr
-        fun to_lazy_ctrT (Type (@{type_name fun}, [T1, T2])) = T1 --> to_lazy_ctrT T2
+        fun to_lazy_ctrT (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) = T1 --> to_lazy_ctrT T2
           | to_lazy_ctrT T = if T = eagerT then lazy_type else raise Match
         val lazy_ctrT = to_lazy_ctrT ctrT
         val argsT = binder_types ctrT
@@ -336,7 +336,7 @@
     val (lazy_case_def, lthy8) =
       let
         val (_, caseT) = dest_Const case'
-        fun to_lazy_caseT (Type (@{type_name fun}, [T1, T2])) =
+        fun to_lazy_caseT (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
             if T1 = eagerT then lazy_type --> T2 else T1 --> to_lazy_caseT T2
         val lazy_caseT = to_lazy_caseT caseT
         val argsT = binder_types lazy_caseT
@@ -379,7 +379,7 @@
 
     val mk_Lazy_delay_eq =
       (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ @{const Unity}))
-      |> mk_eq |> all_abs [@{typ unit} --> lazy_type]
+      |> 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}])
       lthy8
@@ -406,7 +406,7 @@
         val n = length argsT
         val lhs = apply_bounds 0 n eager_ctr
         val rhs = #const lazy_ctr_def $ 
-          (mk_delay (Abs (Name.uu, @{typ unit}, apply_bounds 1 (n + 1) lazy_ctr)))
+          (mk_delay (Abs (Name.uu, \<^typ>\<open>unit\<close>, apply_bounds 1 (n + 1) lazy_ctr)))
       in
         (lhs, rhs) |> mk_eq |> all_abs argsT
       end
@@ -493,7 +493,7 @@
 
     val delay_dummy_thm = (pat_def_thm RS @{thm symmetric})
       |> Drule.infer_instantiate' lthy10
-         [SOME (Thm.cterm_of lthy10 (Const (@{const_name "Pure.dummy_pattern"}, HOLogic.unitT --> lazy_type)))]
+         [SOME (Thm.cterm_of lthy10 (Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, HOLogic.unitT --> lazy_type)))]
       |> Thm.generalize (map (fst o dest_TFree) type_args, []) (Variable.maxidx_of lthy10 + 1);
 
     val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms
@@ -552,7 +552,7 @@
 
       val ((code_eqs, nbe_eqs), pure) =
         ((case hd eqs |> fst |> Thm.prop_of of
-            Const (@{const_name Pure.eq}, _) $ _ $ _ =>
+            Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ =>
               (map (apfst (fn x => x RS @{thm meta_eq_to_obj_eq})) eqs, true)
          | _ => (eqs, false))
         |> apfst (List.partition snd))
@@ -600,7 +600,7 @@
           Syntax.pretty_term ctxt (#destr info),
           Pretty.str ":",
           Pretty.brk 1,
-          Syntax.pretty_typ ctxt (Type (@{type_name lazy}, [#lazyT info])),
+          Syntax.pretty_typ ctxt (Type (\<^type_name>\<open>lazy\<close>, [#lazyT info])),
           Pretty.str ")"
         ]
       ],
@@ -633,27 +633,27 @@
 
 
 val _ =
-  Outer_Syntax.command @{command_keyword code_lazy_type}
+  Outer_Syntax.command \<^command_keyword>\<open>code_lazy_type\<close>
     "make a lazy copy of the datatype and activate substitution"
     (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> code_lazy_type)));
 val _ =
-  Outer_Syntax.command @{command_keyword activate_lazy_type}
+  Outer_Syntax.command \<^command_keyword>\<open>activate_lazy_type\<close>
     "activate substitution on a specific (lazy) type"
     (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> activate_lazy_type)));
 val _ =
-  Outer_Syntax.command @{command_keyword deactivate_lazy_type}
+  Outer_Syntax.command \<^command_keyword>\<open>deactivate_lazy_type\<close>
     "deactivate substitution on a specific (lazy) type"
     (Parse.binding >> (fn b => Toplevel.theory (Binding.name_of b |> deactivate_lazy_type)));
 val _ =
-  Outer_Syntax.command @{command_keyword activate_lazy_types}
+  Outer_Syntax.command \<^command_keyword>\<open>activate_lazy_types\<close>
     "activate substitution on all (lazy) types"
     (pair (Toplevel.theory activate_lazy_types));
 val _ =
-  Outer_Syntax.command @{command_keyword deactivate_lazy_types}
+  Outer_Syntax.command \<^command_keyword>\<open>deactivate_lazy_types\<close>
     "deactivate substitution on all (lazy) type"
     (pair (Toplevel.theory deactivate_lazy_types));
 val _ =
-  Outer_Syntax.command @{command_keyword print_lazy_types}
+  Outer_Syntax.command \<^command_keyword>\<open>print_lazy_types\<close>
     "print the types that have been declared as lazy and their substitution state"
     (pair (Toplevel.theory (tap print_lazy_types)));