diff -r ff6f60e6ab85 -r 1a0c129bb2e0 src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Sequents/ILL.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/ILL.thy
-    ID:         $Id$
     Author:     Sara Kalvala and Valeria de Paiva
     Copyright   1995  University of Cambridge
 *)
@@ -32,19 +31,21 @@
   PromAux :: "three_seqi"
 
 syntax
-  "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
-  "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
-  "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
+  "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
+  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
+  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
 
 parse_translation {*
-  [("@Trueprop", single_tr "Trueprop"),
-   ("@Context", two_seq_tr "Context"),
-   ("@PromAux", three_seq_tr "PromAux")] *}
+  [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
+   (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
+   (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
+*}
 
 print_translation {*
-  [("Trueprop", single_tr' "@Trueprop"),
-   ("Context", two_seq_tr'"@Context"),
-   ("PromAux", three_seq_tr'"@PromAux")] *}
+  [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
+   (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
+   (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
+*}
 
 defs