--- a/src/Sequents/S43.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/Sequents/S43.thy Fri Jan 04 23:22:53 2019 +0100
@@ -20,16 +20,16 @@
let
val tr = seq_tr;
fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
- Const (@{const_syntax S43pi}, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
- in [(@{syntax_const "_S43pi"}, K s43pi_tr)] end
+ Const (\<^const_syntax>\<open>S43pi\<close>, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
+ in [(\<^syntax_const>\<open>_S43pi\<close>, K s43pi_tr)] end
\<close>
print_translation \<open>
let
val tr' = seq_tr';
fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
- Const(@{syntax_const "_S43pi"}, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
-in [(@{const_syntax S43pi}, K s43pi_tr')] end
+ Const(\<^syntax_const>\<open>_S43pi\<close>, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
+in [(\<^const_syntax>\<open>S43pi\<close>, K s43pi_tr')] end
\<close>
axiomatization where