diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
     Copyright   2003  University of Cambridge
 *)
 
-section{*Comprehensive UNITY Theory*}
+section\<open>Comprehensive UNITY Theory\<close>
 
 theory UNITY_Main
 imports Detects PPROD Follows ProgressSets
@@ -11,19 +11,19 @@
 
 ML_file "UNITY_tactics.ML"
 
-method_setup safety = {*
-    Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
+method_setup safety = \<open>
+    Scan.succeed (SIMPLE_METHOD' o constrains_tac)\<close>
     "for proving safety properties"
 
-method_setup ensures_tac = {*
+method_setup ensures_tac = \<open>
   Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
-*} "for proving progress properties"
+\<close> "for proving progress properties"
 
-setup {*
+setup \<open>
   map_theory_simpset (fn ctxt => ctxt
     addsimps (make_o_equivs ctxt @{thm fst_o_funPair} @ make_o_equivs ctxt @{thm snd_o_funPair})
     addsimps (make_o_equivs ctxt @{thm fst_o_lift_map} @ make_o_equivs ctxt @{thm snd_o_lift_map}))
-*}
+\<close>
 
 end