diff -r ff6f60e6ab85 -r 1a0c129bb2e0 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Sequents/Sequents.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/Sequents.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
@@ -36,14 +35,14 @@
 
 
 syntax
- SeqEmp         :: seq                                  ("")
- SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
+ "_SeqEmp"         :: seq                                  ("")
+ "_SeqApp"         :: "[seqobj,seqcont] => seq"            ("__")
 
- SeqContEmp     :: seqcont                              ("")
- SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
+ "_SeqContEmp"     :: seqcont                              ("")
+ "_SeqContApp"     :: "[seqobj,seqcont] => seqcont"        (",/ __")
 
- SeqO           :: "o => seqobj"                        ("_")
- SeqId          :: "'a => seqobj"                       ("$_")
+ "_SeqO"           :: "o => seqobj"                        ("_")
+ "_SeqId"          :: "'a => seqobj"                       ("$_")
 
 types
  single_seqe = "[seq,seqobj] => prop"
@@ -60,86 +59,76 @@
 
 syntax
   (*Constant to allow definitions of SEQUENCES of formulas*)
-  "@Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
+  "_Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
 
 ML {*
 
 (* parse translation for sequences *)
 
-fun abs_seq' t = Abs("s", Type("seq'",[]), t);
+fun abs_seq' t = Abs ("s", Type ("seq'", []), t);   (* FIXME @{type_syntax} *)
 
-fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
-    seqobj_tr(_ $ i) = i;
-
-fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
-    seqcont_tr(Const("SeqContApp",_) $ so $ sc) =
-      (seqobj_tr so) $ (seqcont_tr sc);
+fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
+      Const (@{const_syntax SeqO'}, dummyT) $ f
+  | seqobj_tr (_ $ i) = i;
 
-fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
-    seq_tr(Const("SeqApp",_) $ so $ sc) =
-      abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
+fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0
+  | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ 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) =
+      abs_seq'(seqobj_tr so $ seqcont_tr sc);
 
-fun singlobj_tr(Const("SeqO",_) $ f) =
-    abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
-
+fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) =
+  abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0);
 
 
 (* print translation for sequences *)
 
 fun seqcont_tr' (Bound 0) =
-      Const("SeqContEmp",dummyT) |
-    seqcont_tr' (Const("SeqO'",_) $ f $ s) =
-      Const("SeqContApp",dummyT) $
-      (Const("SeqO",dummyT) $ f) $
-      (seqcont_tr' s) |
-(*    seqcont_tr' ((a as Abs(_,_,_)) $ s)=
-      seqcont_tr'(Term.betapply(a,s)) | *)
-    seqcont_tr' (i $ s) =
-      Const("SeqContApp",dummyT) $
-      (Const("SeqId",dummyT) $ i) $
-      (seqcont_tr' s);
+      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
+  | seqcont_tr' (i $ s) =
+      Const (@{syntax_const "_SeqContApp"}, dummyT) $
+        (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s;
 
 fun seq_tr' s =
-    let fun seq_itr' (Bound 0) =
-              Const("SeqEmp",dummyT) |
-            seq_itr' (Const("SeqO'",_) $ f $ s) =
-              Const("SeqApp",dummyT) $
-              (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
-(*            seq_itr' ((a as Abs(_,_,_)) $ s) =
-              seq_itr'(Term.betapply(a,s)) |    *)
-            seq_itr' (i $ s) =
-              Const("SeqApp",dummyT) $
-              (Const("SeqId",dummyT) $ i) $
-              (seqcont_tr' s)
-    in case s of
-         Abs(_,_,t) => seq_itr' t |
-         _ => s $ (Bound 0)
-    end;
+  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
+      | seq_itr' (i $ s) =
+          Const (@{syntax_const "_SeqApp"}, dummyT) $
+            (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s
+  in
+    case s of
+      Abs (_, _, t) => seq_itr' t
+    | _ => s $ Bound 0
+  end;
 
 
+fun single_tr c [s1, s2] =
+  Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
+
+fun two_seq_tr c [s1, s2] =
+  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
+
+fun three_seq_tr c [s1, s2, s3] =
+  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
+
+fun four_seq_tr c [s1, s2, s3, s4] =
+  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
 
 
-fun single_tr c [s1,s2] =
-    Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
-
-fun two_seq_tr c [s1,s2] =
-    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
-
-fun three_seq_tr c [s1,s2,s3] =
-    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
-
-fun four_seq_tr c [s1,s2,s3,s4] =
-    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
-
-
-fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
-    singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
+fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm
+  | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id;
 
 
 fun single_tr' c [s1, s2] =
-(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 );
-
+  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
 
 fun two_seq_tr' c [s1, s2] =
   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
@@ -157,7 +146,7 @@
 fun side_tr [s1] = seq_tr s1;
 *}
 
-parse_translation {* [("@Side", side_tr)] *}
+parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
 
 use "prover.ML"