diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/RG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Dec 27 19:51:55 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sat Dec 27 20:32:06 2014 +0100
@@ -1,4 +1,4 @@
-section {* Concrete Syntax *}
+section \<open>Concrete Syntax\<close>
 
 theory RG_Syntax
 imports RG_Hoare Quote_Antiquote
@@ -45,17 +45,17 @@
 translations
   "_prg_scheme j i k c" \<rightleftharpoons> "(CONST map (\<lambda>i. c) [j..<k])"
 
-text {* Translations for variables before and after a transition: *}
+text \<open>Translations for variables before and after a transition:\<close>
 
-syntax 
+syntax
   "_before" :: "id \<Rightarrow> 'a" ("\<ordmasculine>_")
   "_after"  :: "id \<Rightarrow> 'a" ("\<ordfeminine>_")
- 
+
 translations
   "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>CONST fst"
   "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>CONST snd"
 
-print_translation {*
+print_translation \<open>
   let
     fun quote_tr' f (t :: ts) =
           Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
@@ -77,6 +77,6 @@
     (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
     (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While"}))]
   end
-*}
+\<close>
 
 end
\ No newline at end of file