diff -r cf7f3465eaf1 -r 240563fbf41d src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/Sequents/Modal0.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -21,20 +21,20 @@
   "_Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
   "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
 
-ML {*
+ML \<open>
   fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
   fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
-*}
+\<close>
 
-parse_translation {*
+parse_translation \<open>
  [(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})),
   (@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))]
-*}
+\<close>
 
-print_translation {*
+print_translation \<open>
  [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})),
   (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
-*}
+\<close>
 
 defs
   strimp_def:    "P --< Q == [](P --> Q)"