diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Hoare/Separation.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -61,24 +61,24 @@
 \<^cancel>\<open>| free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps\<close>
   | free_tr t = t
 
-fun emp_tr [] = Syntax.const @{const_syntax is_empty} $ Syntax.free "H"
+fun emp_tr [] = Syntax.const \<^const_syntax>\<open>is_empty\<close> $ Syntax.free "H"
   | emp_tr ts = raise TERM ("emp_tr", ts);
-fun singl_tr [p, q] = Syntax.const @{const_syntax singl} $ Syntax.free "H" $ p $ q
+fun singl_tr [p, q] = Syntax.const \<^const_syntax>\<open>singl\<close> $ Syntax.free "H" $ p $ q
   | singl_tr ts = raise TERM ("singl_tr", ts);
-fun star_tr [P,Q] = Syntax.const @{const_syntax star} $
+fun star_tr [P,Q] = Syntax.const \<^const_syntax>\<open>star\<close> $
       absfree ("H", dummyT) (free_tr P) $ absfree ("H", dummyT) (free_tr Q) $
       Syntax.free "H"
   | star_tr ts = raise TERM ("star_tr", ts);
-fun wand_tr [P, Q] = Syntax.const @{const_syntax wand} $
+fun wand_tr [P, Q] = Syntax.const \<^const_syntax>\<open>wand\<close> $
       absfree ("H", dummyT) P $ absfree ("H", dummyT) Q $ Syntax.free "H"
   | wand_tr ts = raise TERM ("wand_tr", ts);
 \<close>
 
 parse_translation \<open>
- [(@{syntax_const "_emp"}, K emp_tr),
-  (@{syntax_const "_singl"}, K singl_tr),
-  (@{syntax_const "_star"}, K star_tr),
-  (@{syntax_const "_wand"}, K wand_tr)]
+ [(\<^syntax_const>\<open>_emp\<close>, K emp_tr),
+  (\<^syntax_const>\<open>_singl\<close>, K singl_tr),
+  (\<^syntax_const>\<open>_star\<close>, K star_tr),
+  (\<^syntax_const>\<open>_wand\<close>, K wand_tr)]
 \<close>
 
 text\<open>Now it looks much better:\<close>
@@ -110,24 +110,24 @@
 \<^cancel>\<open>| strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps\<close>
   | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
   | strip (Abs(_,_,P)) = P
-  | strip (Const(@{const_syntax is_empty},_)) = Syntax.const @{syntax_const "_emp"}
+  | strip (Const(\<^const_syntax>\<open>is_empty\<close>,_)) = Syntax.const \<^syntax_const>\<open>_emp\<close>
   | strip t = t;
 
 in
 
-fun is_empty_tr' [_] = Syntax.const @{syntax_const "_emp"}
-fun singl_tr' [_,p,q] = Syntax.const @{syntax_const "_singl"} $ p $ q
-fun star_tr' [P,Q,_] = Syntax.const @{syntax_const "_star"} $ strip P $ strip Q
-fun wand_tr' [P,Q,_] = Syntax.const @{syntax_const "_wand"} $ strip P $ strip Q
+fun is_empty_tr' [_] = Syntax.const \<^syntax_const>\<open>_emp\<close>
+fun singl_tr' [_,p,q] = Syntax.const \<^syntax_const>\<open>_singl\<close> $ p $ q
+fun star_tr' [P,Q,_] = Syntax.const \<^syntax_const>\<open>_star\<close> $ strip P $ strip Q
+fun wand_tr' [P,Q,_] = Syntax.const \<^syntax_const>\<open>_wand\<close> $ strip P $ strip Q
 
 end
 \<close>
 
 print_translation \<open>
- [(@{const_syntax is_empty}, K is_empty_tr'),
-  (@{const_syntax singl}, K singl_tr'),
-  (@{const_syntax star}, K star_tr'),
-  (@{const_syntax wand}, K wand_tr')]
+ [(\<^const_syntax>\<open>is_empty\<close>, K is_empty_tr'),
+  (\<^const_syntax>\<open>singl\<close>, K singl_tr'),
+  (\<^const_syntax>\<open>star\<close>, K star_tr'),
+  (\<^const_syntax>\<open>wand\<close>, K wand_tr')]
 \<close>
 
 text\<open>Now the intermediate proof states are also readable:\<close>