src/Sequents/Sequents.thy

--- a/src/Sequents/Sequents.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/Sequents/Sequents.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -58,44 +58,44 @@
 
 (* parse translation for sequences *)
 
-fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t);
+fun abs_seq' t = Abs ("s", Type (\<^type_name>\<open>seq'\<close>, []), t);
 
-fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
-      Const (@{const_syntax SeqO'}, dummyT) $ f
+fun seqobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>, _) $ f) =
+      Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f
   | seqobj_tr (_ $ i) = i;
 
-fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0
-  | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) =
+fun seqcont_tr (Const (\<^syntax_const>\<open>_SeqContEmp\<close>, _)) = Bound 0
+  | seqcont_tr (Const (\<^syntax_const>\<open>_SeqContApp\<close>, _) $ so $ sc) =
       seqobj_tr so $ seqcont_tr sc;
 
-fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0)
-  | seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) =
+fun seq_tr (Const (\<^syntax_const>\<open>_SeqEmp\<close>, _)) = abs_seq' (Bound 0)
+  | seq_tr (Const (\<^syntax_const>\<open>_SeqApp\<close>, _) $ so $ sc) =
       abs_seq'(seqobj_tr so $ seqcont_tr sc);
 
-fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) =
-  abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0);
+fun singlobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>,_) $ f) =
+  abs_seq' ((Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f) $ Bound 0);
 
 
 (* print translation for sequences *)
 
 fun seqcont_tr' (Bound 0) =
-      Const (@{syntax_const "_SeqContEmp"}, dummyT)
-  | seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
-      Const (@{syntax_const "_SeqContApp"}, dummyT) $
-        (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
+      Const (\<^syntax_const>\<open>_SeqContEmp\<close>, dummyT)
+  | seqcont_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) =
+      Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
+        (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
   | seqcont_tr' (i $ s) =
-      Const (@{syntax_const "_SeqContApp"}, dummyT) $
-        (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s;
+      Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $
+        (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s;
 
 fun seq_tr' s =
   let
-    fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT)
-      | seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
-          Const (@{syntax_const "_SeqApp"}, dummyT) $
-            (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
+    fun seq_itr' (Bound 0) = Const (\<^syntax_const>\<open>_SeqEmp\<close>, dummyT)
+      | seq_itr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) =
+          Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
+            (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s
       | seq_itr' (i $ s) =
-          Const (@{syntax_const "_SeqApp"}, dummyT) $
-            (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s
+          Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $
+            (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s
   in
     case s of
       Abs (_, _, t) => seq_itr' t
@@ -116,8 +116,8 @@
   Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
 
 
-fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm
-  | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id;
+fun singlobj_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>,_) $ fm) = fm
+  | singlobj_tr' id = Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ id;
 
 
 fun single_tr' c [s1, s2] =
@@ -139,7 +139,7 @@
 fun side_tr [s1] = seq_tr s1;
 \<close>
 
-parse_translation \<open>[(@{syntax_const "_Side"}, K side_tr)]\<close>
+parse_translation \<open>[(\<^syntax_const>\<open>_Side\<close>, K side_tr)]\<close>
 
 
 subsection \<open>Proof tools\<close>