src/Sequents/Modal0.thy

 syntax
   "_Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
   "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
 
 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;
+  fun star_tr c [s1, s2] = Syntax.const c $ seq_tr s1 $ seq_tr s2;
+  fun star_tr' c [s1, s2] = Syntax.const c $ seq_tr' s1 $ seq_tr' s2;
 \<close>
 
 parse_translation \<open>
  [(\<^syntax_const>\<open>_Lstar\<close>, K (star_tr \<^const_syntax>\<open>Lstar\<close>)),
   (\<^syntax_const>\<open>_Rstar\<close>, K (star_tr \<^const_syntax>\<open>Rstar\<close>))]