# HG changeset patch
# User wenzelm
# Date 1265928638 -3600
# Node ID b271a8996f26df384e9c5a66c89a128043c1b1e1
# Parent  724e8f77806ab6abe39ec519aa0deecbbda675f1# Parent  446c5063e4fdcdd9b2abb56326c447844e4fd920
merged

diff -r 724e8f77806a -r b271a8996f26 NEWS
--- a/NEWS	Thu Feb 11 12:26:50 2010 -0800
+++ b/NEWS	Thu Feb 11 23:50:38 2010 +0100
@@ -132,6 +132,9 @@
 
 *** ML ***
 
+* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
+syntax constant (cf. 'syntax' command).
+
 * Renamed old-style Drule.standard to Drule.export_without_context, to
 emphasize that this is in no way a standard operation.
 INCOMPATIBILITY.
diff -r 724e8f77806a -r b271a8996f26 doc-src/Classes/Thy/Setup.thy
--- a/doc-src/Classes/Thy/Setup.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/doc-src/Classes/Thy/Setup.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -18,17 +18,19 @@
     fun alpha_ast_tr [] = Syntax.Variable "'a"
       | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
     fun alpha_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
+      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast]
       | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
     fun beta_ast_tr [] = Syntax.Variable "'b"
       | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
     fun beta_ofsort_ast_tr [ast] =
-      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
+      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast]
       | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
-  in [
-    ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
-    ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
-  ] end
+  in
+   [(@{syntax_const "_alpha"}, alpha_ast_tr),
+    (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
+    (@{syntax_const "_beta"}, beta_ast_tr),
+    (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
+  end
 *}
 
 end
\ No newline at end of file
diff -r 724e8f77806a -r b271a8996f26 doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/doc-src/TutorialI/Protocol/Message.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -82,14 +82,14 @@
 (*<*)
 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
 syntax
-  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
+  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
 
 syntax (xsymbols)
-  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
 
 translations
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
-  "{|x, y|}"      == "MPair x y"
+  "{|x, y|}"      == "CONST MPair x y"
 
 
 constdefs
diff -r 724e8f77806a -r b271a8996f26 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/CCL/Set.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -27,17 +27,17 @@
   empty         :: "'a set"                             ("{}")
 
 syntax
-  "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
+  "_Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
 
   (* Big Intersection / Union *)
 
-  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
-  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
+  "_INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
+  "_UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
 
   (* Bounded Quantifiers *)
 
-  "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
-  "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
+  "_Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
+  "_Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
 
 translations
   "{x. P}"      == "CONST Collect(%x. P)"
diff -r 724e8f77806a -r b271a8996f26 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/CCL/Term.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -40,16 +40,16 @@
   letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
 
 syntax
-  "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
+  "_let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
                         [0,0,60] 60)
 
-  "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
+  "_letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
                         [0,0,0,60] 60)
 
-  "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
+  "_letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
                         [0,0,0,0,60] 60)
 
-  "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
+  "_letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
                         [0,0,0,0,0,60] 60)
 
 ML {*
@@ -58,29 +58,30 @@
 (* FIXME does not handle "_idtdummy" *)
 (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
 
-fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
+fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
 fun let_tr' [a,Abs(id,T,b)] =
      let val (id',b') = variant_abs(id,T,b)
-     in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
+     in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
 
 fun letrec_tr [Free(f,S),Free(x,T),a,b] =
-      Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
+      Const(@{const_syntax letrec},dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
 fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
-      Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
+      Const(@{const_syntax letrec2},dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
 fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
-      Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
+      Const(@{const_syntax letrec3},dummyT) $
+        absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
 
 fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
      let val (f',b')  = variant_abs(ff,SS,b)
          val (_,a'') = variant_abs(f,S,a)
          val (x',a')  = variant_abs(x,T,a'')
-     in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
+     in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
 fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
      let val (f',b') = variant_abs(ff,SS,b)
          val ( _,a1) = variant_abs(f,S,a)
          val (y',a2) = variant_abs(y,U,a1)
          val (x',a') = variant_abs(x,T,a2)
-     in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
+     in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
       end;
 fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
      let val (f',b') = variant_abs(ff,SS,b)
@@ -88,22 +89,24 @@
          val (z',a2) = variant_abs(z,V,a1)
          val (y',a3) = variant_abs(y,U,a2)
          val (x',a') = variant_abs(x,T,a3)
-     in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
+     in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
       end;
 
 *}
 
 parse_translation {*
-  [("@let",       let_tr),
-   ("@letrec",    letrec_tr),
-   ("@letrec2",   letrec2_tr),
-   ("@letrec3",   letrec3_tr)] *}
+ [(@{syntax_const "_let"}, let_tr),
+  (@{syntax_const "_letrec"}, letrec_tr),
+  (@{syntax_const "_letrec2"}, letrec2_tr),
+  (@{syntax_const "_letrec3"}, letrec3_tr)]
+*}
 
 print_translation {*
-  [("let",       let_tr'),
-   ("letrec",    letrec_tr'),
-   ("letrec2",   letrec2_tr'),
-   ("letrec3",   letrec3_tr')] *}
+ [(@{const_syntax let}, let_tr'),
+  (@{const_syntax letrec}, letrec_tr'),
+  (@{const_syntax letrec2}, letrec2_tr'),
+  (@{const_syntax letrec3}, letrec3_tr')]
+*}
 
 consts
   napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
diff -r 724e8f77806a -r b271a8996f26 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/CCL/Type.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -28,15 +28,15 @@
   SPLIT         :: "[i, [i, i] => i set] => i set"
 
 syntax
-  "@Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
+  "_Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
                                 [0,0,60] 60)
 
-  "@Sigma"      :: "[idt, i set, i set] => i set"    ("(3SUM _:_./ _)"
+  "_Sigma"      :: "[idt, i set, i set] => i set"    ("(3SUM _:_./ _)"
                                 [0,0,60] 60)
 
-  "@->"         :: "[i set, i set] => i set"         ("(_ ->/ _)"  [54, 53] 53)
-  "@*"          :: "[i set, i set] => i set"         ("(_ */ _)" [56, 55] 55)
-  "@Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
+  "_arrow"      :: "[i set, i set] => i set"         ("(_ ->/ _)"  [54, 53] 53)
+  "_star"       :: "[i set, i set] => i set"         ("(_ */ _)" [56, 55] 55)
+  "_Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
 
 translations
   "PROD x:A. B" => "CONST Pi(A, %x. B)"
@@ -46,8 +46,9 @@
   "{x: A. B}"   == "CONST Subtype(A, %x. B)"
 
 print_translation {*
-  [(@{const_syntax Pi}, dependent_tr' ("@Pi", "@->")),
-   (@{const_syntax Sigma}, dependent_tr' ("@Sigma", "@*"))] *}
+ [(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
+  (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
+*}
 
 axioms
   Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
diff -r 724e8f77806a -r b271a8996f26 src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Cube/Cube.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Cube/Cube.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
 *)
 
@@ -54,7 +53,9 @@
   Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
   arrow         :: "[term, term] => term"               (infixr "\<rightarrow>" 10)
 
-print_translation {* [(@{const_syntax Prod}, dependent_tr' ("Pi", "arrow"))] *}
+print_translation {*
+  [(@{const_syntax Prod}, dependent_tr' (@{syntax_const Pi}, @{syntax_const arrow}))]
+*}
 
 axioms
   s_b:          "*: []"
diff -r 724e8f77806a -r b271a8996f26 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/FOLP/IFOLP.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -22,7 +22,6 @@
 
 consts
       (*** Judgements ***)
- "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
  Proof          ::   "[o,p]=>prop"
  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
 
@@ -66,6 +65,8 @@
 
 local
 
+syntax "_Proof" :: "[p,o]=>prop"    ("(_ /: _)" [51, 10] 5)
+
 ML {*
 
 (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
@@ -74,12 +75,12 @@
 fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
 
 fun proof_tr' [P,p] =
-    if !show_proofs then Const("@Proof",dummyT) $ p $ P
-    else P  (*this case discards the proof term*);
+  if ! show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
+  else P  (*this case discards the proof term*);
 *}
 
-parse_translation {* [("@Proof", proof_tr)] *}
-print_translation {* [("Proof", proof_tr')] *}
+parse_translation {* [(@{syntax_const "_Proof"}, proof_tr)] *}
+print_translation {* [(@{const_syntax Proof}, proof_tr')] *}
 
 axioms
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Auth/Message.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -51,10 +51,10 @@
 
 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
 syntax
-  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
+  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
 
 syntax (xsymbols)
-  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
 
 translations
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Complete_Lattice.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -106,10 +106,10 @@
   "INF x. B"     == "INF x:CONST UNIV. B"
   "INF x:A. B"   == "CONST INFI A (%x. B)"
 
-print_translation {* [
-Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} "_SUP",
-Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} "_INF"
-] *} -- {* to avoid eta-contraction of body *}
+print_translation {*
+  [Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"},
+    Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}]
+*} -- {* to avoid eta-contraction of body *}
 
 context complete_lattice
 begin
@@ -282,16 +282,16 @@
   "UNION \<equiv> SUPR"
 
 syntax
-  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
-  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
+  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
+  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
 
 syntax (xsymbols)
-  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
-  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
+  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
+  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
 
 syntax (latex output)
-  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
-  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
 
 translations
   "UN x y. B"   == "UN x. UN y. B"
@@ -308,9 +308,9 @@
   subscripts in Proof General.
 *}
 
-print_translation {* [
-Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"
-] *} -- {* to avoid eta-contraction of body *}
+print_translation {*
+  [Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
+*} -- {* to avoid eta-contraction of body *}
 
 lemma UNION_eq_Union_image:
   "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
@@ -518,16 +518,16 @@
   "INTER \<equiv> INFI"
 
 syntax
-  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
-  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
+  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
+  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
 
 syntax (xsymbols)
-  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
-  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
+  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
+  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
 
 syntax (latex output)
-  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
-  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
 
 translations
   "INT x y. B"  == "INT x. INT y. B"
@@ -535,9 +535,9 @@
   "INT x. B"    == "INT x:CONST UNIV. B"
   "INT x:A. B"  == "CONST INTER A (%x. B)"
 
-print_translation {* [
-Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"
-] *} -- {* to avoid eta-contraction of body *}
+print_translation {*
+  [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
+*} -- {* to avoid eta-contraction of body *}
 
 lemma INTER_eq_Inter_image:
   "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Finite_Set.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1095,13 +1095,16 @@
 
 print_translation {*
 let
-  fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
-    if x<>y then raise Match
-    else let val x' = Syntax.mark_bound x
-             val t' = subst_bound(x',t)
-             val P' = subst_bound(x',P)
-         in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
-in [("setsum", setsum_tr')] end
+  fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
+        if x <> y then raise Match
+        else
+          let
+            val x' = Syntax.mark_bound x;
+            val t' = subst_bound (x', t);
+            val P' = subst_bound (x', P);
+          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
+    | setsum_tr' _ = raise Match;
+in [(@{const_syntax setsum}, setsum_tr')] end
 *}
 
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Fun.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -387,18 +387,16 @@
   "_updbind" :: "['a, 'a] => updbind"             ("(2_ :=/ _)")
   ""         :: "updbind => updbinds"             ("_")
   "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _")
-  "_Update"  :: "['a, updbinds] => 'a"            ("_/'((_)')" [1000,0] 900)
+  "_Update"  :: "['a, updbinds] => 'a"            ("_/'((_)')" [1000, 0] 900)
 
 translations
-  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
-  "f(x:=y)"                     == "fun_upd f x y"
+  "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
+  "f(x:=y)" == "CONST fun_upd f x y"
 
 (* Hint: to define the sum of two functions (or maps), use sum_case.
          A nice infix syntax could be defined (in Datatype.thy or below) by
-consts
-  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
-translations
- "fun_sum" == sum_case
+notation
+  sum_case  (infixr "'(+')"80)
 *)
 
 lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/HOL.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -129,16 +129,15 @@
   "_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
 
 translations
-  "THE x. P"              == "The (%x. P)"
+  "THE x. P"              == "CONST The (%x. P)"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
-  "let x = a in e"        == "Let a (%x. e)"
+  "let x = a in e"        == "CONST Let a (%x. e)"
 
 print_translation {*
-(* To avoid eta-contraction of body: *)
-[("The", fn [Abs abs] =>
-     let val (x,t) = atomic_abs_tr' abs
-     in Syntax.const "_The" $ x $ t end)]
-*}
+  [(@{const_syntax The}, fn [Abs abs] =>
+      let val (x, t) = atomic_abs_tr' abs
+      in Syntax.const @{syntax_const "_The"} $ x $ t end)]
+*}  -- {* To avoid eta-contraction of body *}
 
 syntax (xsymbols)
   "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hilbert_Choice.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -25,11 +25,10 @@
   "SOME x. P" == "CONST Eps (%x. P)"
 
 print_translation {*
-(* to avoid eta-contraction of body *)
-[(@{const_syntax Eps}, fn [Abs abs] =>
-     let val (x,t) = atomic_abs_tr' abs
-     in Syntax.const "_Eps" $ x $ t end)]
-*}
+  [(@{const_syntax Eps}, fn [Abs abs] =>
+      let val (x, t) = atomic_abs_tr' abs
+      in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
+*} -- {* to avoid eta-contraction of body *}
 
 definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
 "inv_into A f == %x. SOME y. y : A & f y = x"
@@ -315,7 +314,7 @@
 syntax
   "_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"    ("LEAST _ WRT _. _" [0, 4, 10] 10)
 translations
-  "LEAST x WRT m. P" == "LeastM m (%x. P)"
+  "LEAST x WRT m. P" == "CONST LeastM m (%x. P)"
 
 lemma LeastMI2:
   "P x ==> (!!y. P y ==> m x <= m y)
@@ -369,11 +368,10 @@
   "Greatest == GreatestM (%x. x)"
 
 syntax
-  "_GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
+  "_GreatestM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"
       ("GREATEST _ WRT _. _" [0, 4, 10] 10)
-
 translations
-  "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
+  "GREATEST x WRT m. P" == "CONST GreatestM m (%x. P)"
 
 lemma GreatestMI2:
   "P x ==> (!!y. P y ==> m y <= m x)
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hoare/HeapSyntax.thy
--- a/src/HOL/Hoare/HeapSyntax.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/HeapSyntax.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -15,9 +15,9 @@
   "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    ("_^._" [65,1000] 65)
 translations
-  "f(r \<rightarrow> v)"  ==  "f(CONST addr r := v)"
-  "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
-  "p^.f"       =>  "f(CONST addr p)"
+  "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
+  "p^.f := e" => "f := f(p \<rightarrow> e)"
+  "p^.f" => "f(CONST addr p)"
 
 
 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hoare/HeapSyntaxAbort.thy
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -23,9 +23,9 @@
   "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    ("_^._" [65,1000] 65)
 translations
-  "_refupdate f r v"  ==  "f(CONST addr r := v)"
-  "p^.f := e"  =>  "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
-  "p^.f"       =>  "f(CONST addr p)"
+  "_refupdate f r v" == "f(CONST addr r := v)"
+  "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
+  "p^.f" => "f(CONST addr p)"
 
 
 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/Hoare.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Hoare/Hoare.thy
-    ID:         $Id$
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   1998 TUM
 
@@ -19,11 +18,11 @@
     'a assn = "'a set"
 
 datatype
- 'a com = Basic "'a \<Rightarrow> 'a"         
+ 'a com = Basic "'a \<Rightarrow> 'a"
    | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
    | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
-  
+
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 types 'a sem = "'a => 'a => bool"
@@ -68,11 +67,11 @@
 
 fun mk_abstuple [x] body = abs (x, body)
   | mk_abstuple (x::xs) body =
-      Syntax.const "split" $ abs (x, mk_abstuple xs body);
+      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
 
 fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
   | mk_fbody a e ((b,_)::xs) =
-      Syntax.const "Pair" $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;
+      Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;
 
 fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
 end
@@ -82,22 +81,22 @@
 (*all meta-variables for bexp except for TRUE are translated as if they
   were boolean expressions*)
 ML{*
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"
-  | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b;
-  
-fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
+fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
+  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
+
+fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
 *}
 (* com_tr *)
 ML{*
-fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
-      Syntax.const "Basic" $ mk_fexp a e xs
-  | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
-  | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
-      Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =
-      Syntax.const "Cond" $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const ("While",_) $ b $ I $ c) xs =
-      Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+fun com_tr (Const(@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
+      Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
+      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
+      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
+      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
   | com_tr t _ = t (* if t is just a Free/Var *)
 *}
 
@@ -106,65 +105,66 @@
 local
 
 fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
-  | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T);
+  | var_tr(Const (@{syntax_const "_constrain"}, _) $ (Free (a,_)) $ T) = (a,T);
 
-fun vars_tr (Const ("_idts", _) $ idt $ vars) = var_tr idt :: vars_tr vars
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
   | vars_tr t = [var_tr t]
 
 in
 fun hoare_vars_tr [vars, pre, prg, post] =
       let val xs = vars_tr vars
-      in Syntax.const "Valid" $
+      in Syntax.const @{const_syntax Valid} $
          assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
       end
   | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
 end
 *}
 
-parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
+parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *}
 
 
 (*****************************************************************************)
 
 (*** print translations ***)
 ML{*
-fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) =
+fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
                             subst_bound (Syntax.free v, dest_abstuple body)
   | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
   | dest_abstuple trm = trm;
 
-fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
   | abs2list (Abs(x,T,t)) = [Free (x, T)]
   | abs2list _ = [];
 
-fun mk_ts (Const ("split",_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
   | mk_ts (Abs(x,_,t)) = mk_ts t
-  | mk_ts (Const ("Pair",_) $ a $ b) = a::(mk_ts b)
+  | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
   | mk_ts t = [t];
 
-fun mk_vts (Const ("split",_) $ (Abs(x,_,t))) = 
+fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
            ((Syntax.free x)::(abs2list t), mk_ts t)
   | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
   | mk_vts t = raise Match;
-  
-fun find_ch [] i xs = (false, (Syntax.free "not_ch",Syntax.free "not_ch" ))
-  | find_ch ((v,t)::vts) i xs = if t=(Bound i) then find_ch vts (i-1) xs
-              else (true, (v, subst_bounds (xs,t)));
-  
-fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true
+
+fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
+  | find_ch ((v,t)::vts) i xs =
+      if t = Bound i then find_ch vts (i-1) xs
+      else (true, (v, subst_bounds (xs, t)));
+
+fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
   | is_f (Abs(x,_,t)) = true
   | is_f t = false;
 *}
 
 (* assn_tr' & bexp_tr'*)
-ML{*  
-fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
-  | assn_tr' (Const (@{const_name inter}, _) $ (Const ("Collect",_) $ T1) $ 
-                                   (Const ("Collect",_) $ T2)) =  
-            Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
+ML{*
+fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
+  | assn_tr' (Const (@{const_syntax inter}, _) $
+        (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) =
+      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
   | assn_tr' t = t;
 
-fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T 
+fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
   | bexp_tr' t = t;
 *}
 
@@ -173,22 +173,24 @@
 fun mk_assign f =
   let val (vs, ts) = mk_vts f;
       val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
-  in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
-     else Syntax.const @{const_syntax annskip} end;
+  in
+    if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
+    else Syntax.const @{const_syntax annskip}
+  end;
 
-fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
-                                           else Syntax.const "Basic" $ f
-  | com_tr' (Const ("Seq",_) $ c1 $ c2) = Syntax.const "Seq" $
-                                                 com_tr' c1 $ com_tr' c2
-  | com_tr' (Const ("Cond",_) $ b $ c1 $ c2) = Syntax.const "Cond" $
-                                           bexp_tr' b $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const ("While",_) $ b $ I $ c) = Syntax.const "While" $
-                                               bexp_tr' b $ assn_tr' I $ com_tr' c
+fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
+      if is_f f then mk_assign f
+      else Syntax.const @{const_syntax Basic} $ f
+  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
+      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
+  | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
+      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
+  | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
+      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
   | com_tr' t = t;
 
-
 fun spec_tr' [p, c, q] =
-  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
+  Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
 *}
 
 print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/HoareAbort.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -20,7 +20,7 @@
    | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
    | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
-  
+
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 types 'a sem = "'a option => 'a option => bool"
@@ -69,11 +69,11 @@
 
 fun mk_abstuple [x] body = abs (x, body)
   | mk_abstuple (x::xs) body =
-      Syntax.const "split" $ abs (x, mk_abstuple xs body);
+      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
 
 fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
   | mk_fbody a e ((b,_)::xs) =
-      Syntax.const "Pair" $ (if a=b then e else free b) $ mk_fbody a e xs;
+      Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs;
 
 fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
 end
@@ -83,22 +83,22 @@
 (*all meta-variables for bexp except for TRUE are translated as if they
   were boolean expressions*)
 ML{*
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"
-  | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b;
-  
-fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
+fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"   (* FIXME !? *)
+  | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
+
+fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
 *}
 (* com_tr *)
 ML{*
-fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
-      Syntax.const "Basic" $ mk_fexp a e xs
-  | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
-  | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
-      Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =
-      Syntax.const "Cond" $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
-  | com_tr (Const ("While",_) $ b $ I $ c) xs =
-      Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+fun com_tr (Const (@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
+      Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+  | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+  | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
+      Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
+      Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
+  | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
+      Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
   | com_tr t _ = t (* if t is just a Free/Var *)
 *}
 
@@ -106,66 +106,67 @@
 ML{*
 local
 
-fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
-  | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T);
+fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
+  | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
 
-fun vars_tr (Const ("_idts", _) $ idt $ vars) = var_tr idt :: vars_tr vars
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
   | vars_tr t = [var_tr t]
 
 in
 fun hoare_vars_tr [vars, pre, prg, post] =
       let val xs = vars_tr vars
-      in Syntax.const "Valid" $
+      in Syntax.const @{const_syntax Valid} $
          assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
       end
   | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
 end
 *}
 
-parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
+parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *}
 
 
 (*****************************************************************************)
 
 (*** print translations ***)
 ML{*
-fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) =
-                            subst_bound (Syntax.free v, dest_abstuple body)
+fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
+      subst_bound (Syntax.free v, dest_abstuple body)
   | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
   | dest_abstuple trm = trm;
 
-fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
   | abs2list (Abs(x,T,t)) = [Free (x, T)]
   | abs2list _ = [];
 
-fun mk_ts (Const ("split",_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
   | mk_ts (Abs(x,_,t)) = mk_ts t
-  | mk_ts (Const ("Pair",_) $ a $ b) = a::(mk_ts b)
+  | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
   | mk_ts t = [t];
 
-fun mk_vts (Const ("split",_) $ (Abs(x,_,t))) = 
+fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
            ((Syntax.free x)::(abs2list t), mk_ts t)
   | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
   | mk_vts t = raise Match;
-  
-fun find_ch [] i xs = (false, (Syntax.free "not_ch",Syntax.free "not_ch" ))
-  | find_ch ((v,t)::vts) i xs = if t=(Bound i) then find_ch vts (i-1) xs
-              else (true, (v, subst_bounds (xs,t)));
-  
-fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true
+
+fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
+  | find_ch ((v,t)::vts) i xs =
+      if t = Bound i then find_ch vts (i-1) xs
+      else (true, (v, subst_bounds (xs,t)));
+
+fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
   | is_f (Abs(x,_,t)) = true
   | is_f t = false;
 *}
 
 (* assn_tr' & bexp_tr'*)
-ML{*  
-fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
-  | assn_tr' (Const (@{const_name inter},_) $ (Const ("Collect",_) $ T1) $ 
-                                   (Const ("Collect",_) $ T2)) =  
-            Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
+ML{*
+fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
+  | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $
+        (Const (@{const_syntax Collect},_) $ T2)) =
+      Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
   | assn_tr' t = t;
 
-fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T 
+fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
   | bexp_tr' t = t;
 *}
 
@@ -174,22 +175,23 @@
 fun mk_assign f =
   let val (vs, ts) = mk_vts f;
       val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
-  in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
-     else Syntax.const @{const_syntax annskip} end;
+  in
+    if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
+    else Syntax.const @{const_syntax annskip}
+  end;
 
-fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
-                                           else Syntax.const "Basic" $ f
-  | com_tr' (Const ("Seq",_) $ c1 $ c2) = Syntax.const "Seq" $
-                                                 com_tr' c1 $ com_tr' c2
-  | com_tr' (Const ("Cond",_) $ b $ c1 $ c2) = Syntax.const "Cond" $
-                                           bexp_tr' b $ com_tr' c1 $ com_tr' c2
-  | com_tr' (Const ("While",_) $ b $ I $ c) = Syntax.const "While" $
-                                               bexp_tr' b $ assn_tr' I $ com_tr' c
+fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
+      if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f
+  | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
+      Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
+  | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
+      Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
+  | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
+      Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
   | com_tr' t = t;
 
-
 fun spec_tr' [p, c, q] =
-  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
+  Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
 *}
 
 print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/Separation.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -64,22 +64,25 @@
 *)
   | free_tr t = t
 
-fun emp_tr [] = Syntax.const "is_empty" $ Syntax.free "H"
+fun emp_tr [] = Syntax.const @{const_syntax is_empty} $ Syntax.free "H"
   | emp_tr ts = raise TERM ("emp_tr", ts);
-fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
+fun singl_tr [p, q] = Syntax.const @{const_syntax singl} $ Syntax.free "H" $ p $ q
   | singl_tr ts = raise TERM ("singl_tr", ts);
-fun star_tr [P,Q] = Syntax.const "star" $
-      absfree("H",dummyT,free_tr P) $ absfree("H",dummyT,free_tr Q) $
+fun star_tr [P,Q] = Syntax.const @{const_syntax star} $
+      absfree ("H", dummyT, free_tr P) $ absfree ("H", dummyT, free_tr Q) $
       Syntax.free "H"
   | star_tr ts = raise TERM ("star_tr", ts);
-fun wand_tr [P,Q] = Syntax.const "wand" $
-      absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
+fun wand_tr [P, Q] = Syntax.const @{const_syntax wand} $
+      absfree ("H", dummyT, P) $ absfree ("H", dummyT, Q) $ Syntax.free "H"
   | wand_tr ts = raise TERM ("wand_tr", ts);
 *}
 
-parse_translation
- {* [("_emp", emp_tr), ("_singl", singl_tr),
-     ("_star", star_tr), ("_wand", wand_tr)] *}
+parse_translation {*
+ [(@{syntax_const "_emp"}, emp_tr),
+  (@{syntax_const "_singl"}, singl_tr),
+  (@{syntax_const "_star"}, star_tr),
+  (@{syntax_const "_wand"}, wand_tr)]
+*}
 
 text{* Now it looks much better: *}
 
@@ -102,17 +105,9 @@
 text{* But the output is still unreadable. Thus we also strip the heap
 parameters upon output: *}
 
-(* debugging code:
-fun sot(Free(s,_)) = s
-  | sot(Var((s,i),_)) = "?" ^ s ^ string_of_int i
-  | sot(Const(s,_)) = s
-  | sot(Bound i) = "B." ^ string_of_int i
-  | sot(s $ t) = "(" ^ sot s ^ " " ^ sot t ^ ")"
-  | sot(Abs(_,_,t)) = "(% " ^ sot t ^ ")";
-*)
+ML {*
+local
 
-ML{*
-local
 fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t
   | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
 (*
@@ -120,19 +115,25 @@
 *)
   | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
   | strip (Abs(_,_,P)) = P
-  | strip (Const("is_empty",_)) = Syntax.const "_emp"
+  | strip (Const(@{const_syntax is_empty},_)) = Syntax.const @{syntax_const "_emp"}
   | strip t = t;
+
 in
-fun is_empty_tr' [_] = Syntax.const "_emp"
-fun singl_tr' [_,p,q] = Syntax.const "_singl" $ p $ q
-fun star_tr' [P,Q,_] = Syntax.const "_star" $ strip P $ strip Q
-fun wand_tr' [P,Q,_] = Syntax.const "_wand" $ strip P $ strip Q
+
+fun is_empty_tr' [_] = Syntax.const @{syntax_const "_emp"}
+fun singl_tr' [_,p,q] = Syntax.const @{syntax_const "_singl"} $ p $ q
+fun star_tr' [P,Q,_] = Syntax.const @{syntax_const "_star"} $ strip P $ strip Q
+fun wand_tr' [P,Q,_] = Syntax.const @{syntax_const "_wand"} $ strip P $ strip Q
+
 end
 *}
 
-print_translation
- {* [("is_empty", is_empty_tr'),("singl", singl_tr'),
-     ("star", star_tr'),("wand", wand_tr')] *}
+print_translation {*
+ [(@{const_syntax is_empty}, is_empty_tr'),
+  (@{const_syntax singl}, singl_tr'),
+  (@{const_syntax star}, star_tr'),
+  (@{const_syntax wand}, wand_tr')]
+*}
 
 text{* Now the intermediate proof states are also readable: *}
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hoare_Parallel/OG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -5,18 +5,25 @@
 text{* Syntax for commands and for assertions and boolean expressions in 
  commands @{text com} and annotated commands @{text ann_com}. *}
 
+abbreviation Skip :: "'a com"  ("SKIP" 63)
+  where "SKIP \<equiv> Basic id"
+
+abbreviation AnnSkip :: "'a assn \<Rightarrow> 'a ann_com"  ("_//SKIP" [90] 63)
+  where "r SKIP \<equiv> AnnBasic r id"
+
+notation
+  Seq  ("_,,/ _" [55, 56] 55) and
+  AnnSeq  ("_;;/ _" [60,61] 60)
+
 syntax
   "_Assign"      :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
   "_AnnAssign"   :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com"    ("(_ \<acute>_ :=/ _)" [90,70,65] 61)
 
 translations
-  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
-  "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
+  "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
+  "r \<acute>x := a" \<rightharpoonup> "CONST AnnBasic r \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
 
 syntax
-  "_AnnSkip"     :: "'a assn \<Rightarrow> 'a ann_com"              ("_//SKIP" [90] 63)
-  "_AnnSeq"      :: "'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com"  ("_;;/ _" [60,61] 60)
-  
   "_AnnCond1"    :: "'a assn \<Rightarrow> 'a bexp  \<Rightarrow> 'a ann_com  \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com"
                     ("_ //IF _ /THEN _ /ELSE _ /FI"  [90,0,0,0] 61)
   "_AnnCond2"    :: "'a assn \<Rightarrow> 'a bexp  \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com"
@@ -28,8 +35,6 @@
   "_AnnAtom"     :: "'a assn  \<Rightarrow> 'a com \<Rightarrow> 'a ann_com"   ("_//\<langle>_\<rangle>" [90,0] 61)
   "_AnnWait"     :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com"   ("_//WAIT _ END" [90,0] 61)
 
-  "_Skip"        :: "'a com"                 ("SKIP" 63)
-  "_Seq"         :: "'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" ("_,,/ _" [55, 56] 55)
   "_Cond"        :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" 
                                   ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
   "_Cond2"       :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"   ("IF _ THEN _ FI" [0,0] 56)
@@ -39,21 +44,16 @@
                     ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
 
 translations
-  "SKIP" \<rightleftharpoons> "Basic id"
-  "c_1,, c_2" \<rightleftharpoons> "Seq c_1 c_2"
-
-  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
+  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
   "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
-  "WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c"
+  "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While .{b}. i c"
   "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
 
-  "r SKIP" \<rightleftharpoons> "AnnBasic r id"
-  "c_1;; c_2" \<rightleftharpoons> "AnnSeq c_1 c_2" 
-  "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "AnnCond1 r .{b}. c1 c2"
-  "r IF b THEN c FI" \<rightharpoonup> "AnnCond2 r .{b}. c"
-  "r WHILE b INV i DO c OD" \<rightharpoonup> "AnnWhile r .{b}. i c"
-  "r AWAIT b THEN c END" \<rightharpoonup> "AnnAwait r .{b}. c"
-  "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT True THEN c END"
+  "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST AnnCond1 r .{b}. c1 c2"
+  "r IF b THEN c FI" \<rightharpoonup> "CONST AnnCond2 r .{b}. c"
+  "r WHILE b INV i DO c OD" \<rightharpoonup> "CONST AnnWhile r .{b}. i c"
+  "r AWAIT b THEN c END" \<rightharpoonup> "CONST AnnAwait r .{b}. c"
+  "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END"
   "r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
  
 nonterminals
@@ -68,29 +68,29 @@
                   ("SCHEME [_ \<le> _ < _] _// _" [0,0,0,60, 90] 57)
 
 translations
-  "_prg c q" \<rightleftharpoons> "[(Some c, q)]"
-  "_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps"
-  "_PAR ps" \<rightleftharpoons> "Parallel ps"
+  "_prg c q" \<rightleftharpoons> "[(CONST Some c, q)]"
+  "_prgs c q ps" \<rightleftharpoons> "(CONST Some c, q) # ps"
+  "_PAR ps" \<rightleftharpoons> "CONST Parallel ps"
 
-  "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (Some c, q)) [j..<k]"
+  "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (CONST Some c, q)) [j..<k]"
 
 print_translation {*
   let
     fun quote_tr' f (t :: ts) =
-          Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
+          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | quote_tr' _ _ = raise Match;
 
     fun annquote_tr' f (r :: t :: ts) =
-          Term.list_comb (f $ r $ Syntax.quote_tr' "_antiquote" t, ts)
+          Term.list_comb (f $ r $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | annquote_tr' _ _ = raise Match;
 
-    val assert_tr' = quote_tr' (Syntax.const "_Assert");
+    val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
 
-    fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
+    fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
-    fun annbexp_tr' name (r :: (Const ("Collect", _) $ t) :: ts) =
+    fun annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) $ t) :: ts) =
           annquote_tr' (Syntax.const name) (r :: t :: ts)
       | annbexp_tr' _ _ = raise Match;
 
@@ -100,41 +100,47 @@
       | NONE => raise Match);
 
     fun update_name_tr' (Free x) = Free (upd_tr' x)
-      | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
+      | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
           c $ Free (upd_tr' x)
       | update_name_tr' (Const x) = Const (upd_tr' x)
       | update_name_tr' _ = raise Match;
 
-    fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
-      | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
+    fun K_tr' (Abs (_, _, t)) =
+          if null (loose_bnos t) then t else raise Match
+      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
+          if null (loose_bnos t) then t else raise Match
       | K_tr' _ = raise Match;
 
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
+          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f)
             (Abs (x, dummyT, K_tr' k) :: ts)
       | assign_tr' _ = raise Match;
 
     fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f)
+          quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ update_name_tr' f)
             (Abs (x, dummyT, K_tr' k) :: ts)
       | annassign_tr' _ = raise Match;
 
-    fun Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1 ) $ t2) $ Const ("Nil",_))] = 
-                   (Syntax.const "_prg" $ t1 $ t2)
-      | Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1) $ t2) $ ts)] =
-                     (Syntax.const "_prgs" $ t1 $ t2 $ Parallel_PAR [ts])
+    fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
+            (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some},_) $ t1 ) $ t2) $
+            Const (@{const_syntax Nil}, _))] = Syntax.const @{syntax_const "_prg"} $ t1 $ t2
+      | Parallel_PAR [(Const (@{const_syntax Cons}, _) $
+            (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some}, _) $ t1) $ t2) $ ts)] =
+          Syntax.const @{syntax_const "_prgs"} $ t1 $ t2 $ Parallel_PAR [ts]
       | Parallel_PAR _ = raise Match;
 
-fun Parallel_tr' ts = Syntax.const "_PAR" $ Parallel_PAR ts;
+    fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} $ Parallel_PAR ts;
   in
-    [("Collect", assert_tr'), ("Basic", assign_tr'), 
-      ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv"),
-      ("AnnBasic", annassign_tr'), 
-      ("AnnWhile", annbexp_tr' "_AnnWhile"), ("AnnAwait", annbexp_tr' "_AnnAwait"),
-      ("AnnCond1", annbexp_tr' "_AnnCond1"), ("AnnCond2", annbexp_tr' "_AnnCond2")]
-
-  end
-
+   [(@{const_syntax Collect}, assert_tr'),
+    (@{const_syntax Basic}, assign_tr'),
+    (@{const_syntax Cond}, bexp_tr' "_Cond"),
+    (@{const_syntax While}, bexp_tr' "_While_inv"),
+    (@{const_syntax AnnBasic}, annassign_tr'),
+    (@{const_syntax AnnWhile}, annbexp_tr' "_AnnWhile"),
+    (@{const_syntax AnnAwait}, annbexp_tr' "_AnnAwait"),
+    (@{const_syntax AnnCond1}, annbexp_tr' "_AnnCond1"),
+    (@{const_syntax AnnCond2}, annbexp_tr' "_AnnCond2")]
+  end;
 *}
 
 end
\ No newline at end of file
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hoare_Parallel/OG_Tran.thy
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -69,7 +69,7 @@
 
 monos "rtrancl_mono"
 
-text {* The corresponding syntax translations are: *}
+text {* The corresponding abbreviations are: *}
 
 abbreviation
   ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a) 
@@ -101,8 +101,8 @@
   SEM :: "'a com \<Rightarrow> 'a set \<Rightarrow> 'a set"
   "SEM c S \<equiv> \<Union>sem c ` S "
 
-syntax "_Omega" :: "'a com"    ("\<Omega>" 63)
-translations  "\<Omega>" \<rightleftharpoons> "While CONST UNIV CONST UNIV (Basic id)"
+abbreviation Omega :: "'a com"    ("\<Omega>" 63)
+  where "\<Omega> \<equiv> While UNIV UNIV (Basic id)"
 
 consts fwhile :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> nat \<Rightarrow> 'a com"
 primrec 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hoare_Parallel/Quote_Antiquote.thy
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -12,13 +12,13 @@
   "_Assert"    :: "'a \<Rightarrow> 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
 
 translations
-  ".{b}." \<rightharpoonup> "Collect \<guillemotleft>b\<guillemotright>"
+  ".{b}." \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
 
 parse_translation {*
   let
-    fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
+    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
       | quote_tr ts = raise TERM ("quote_tr", ts);
-  in [("_quote", quote_tr)] end
+  in [(@{syntax_const "_quote"}, quote_tr)] end
 *}
 
 end
\ No newline at end of file
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Hoare_Parallel/RG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -4,10 +4,13 @@
 imports RG_Hoare Quote_Antiquote
 begin
 
+abbreviation Skip :: "'a com"  ("SKIP")
+  where "SKIP \<equiv> Basic id"
+
+notation Seq  ("(_;;/ _)" [60,61] 60)
+
 syntax
   "_Assign"    :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"                     ("(\<acute>_ :=/ _)" [70, 65] 61)
-  "_skip"      :: "'a com"                                  ("SKIP")
-  "_Seq"       :: "'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"              ("(_;;/ _)" [60,61] 60)
   "_Cond"      :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"   ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)
   "_Cond2"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0IF _ THEN _ FI)" [0,0] 56)
   "_While"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0WHILE _ /DO _ /OD)"  [0, 0] 61)
@@ -16,14 +19,12 @@
   "_Wait"      :: "'a bexp \<Rightarrow> 'a com"                       ("(0WAIT _ END)" 61)
 
 translations
-  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
-  "SKIP" \<rightleftharpoons> "Basic id"
-  "c1;; c2" \<rightleftharpoons> "Seq c1 c2"
-  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
+  "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
+  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
   "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
-  "WHILE b DO c OD" \<rightharpoonup> "While .{b}. c"
-  "AWAIT b THEN c END" \<rightleftharpoons> "Await .{b}. c"
-  "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT True THEN c END"
+  "WHILE b DO c OD" \<rightharpoonup> "CONST While .{b}. c"
+  "AWAIT b THEN c END" \<rightleftharpoons> "CONST Await .{b}. c"
+  "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END"
   "WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"
 
 nonterminals
@@ -52,18 +53,18 @@
   "_after"  :: "id \<Rightarrow> 'a" ("\<ordfeminine>_")
  
 translations
-  "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>fst"
-  "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>snd"
+  "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>CONST fst"
+  "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>CONST snd"
 
 print_translation {*
   let
     fun quote_tr' f (t :: ts) =
-          Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
+          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | quote_tr' _ _ = raise Match;
 
-    val assert_tr' = quote_tr' (Syntax.const "_Assert");
+    val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
 
-    fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
+    fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
@@ -73,22 +74,26 @@
       | NONE => raise Match);
 
     fun update_name_tr' (Free x) = Free (upd_tr' x)
-      | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
+      | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
           c $ Free (upd_tr' x)
       | update_name_tr' (Const x) = Const (upd_tr' x)
       | update_name_tr' _ = raise Match;
 
-    fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
-      | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
+    fun K_tr' (Abs (_, _, t)) =
+          if null (loose_bnos t) then t else raise Match
+      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
+          if null (loose_bnos t) then t else raise Match
       | K_tr' _ = raise Match;
 
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
+          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f)
             (Abs (x, dummyT, K_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
-    [("Collect", assert_tr'), ("Basic", assign_tr'),
-      ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]
+   [(@{const_syntax Collect}, assert_tr'),
+    (@{const_syntax Basic}, assign_tr'),
+    (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
+    (@{const_syntax While}, bexp_tr' @{syntax_const "_While"})]
   end
 *}
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -147,16 +147,16 @@
           val v_used = fold_aterms
             (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
         in if v_used then
-          Const ("_bindM", dummyT) $ v $ f $ unfold_monad g'
+          Const (@{syntax_const "_bindM"}, dummyT) $ v $ f $ unfold_monad g'
         else
-          Const ("_chainM", dummyT) $ f $ unfold_monad g'
+          Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g'
         end
     | unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) =
-        Const ("_chainM", dummyT) $ f $ unfold_monad g
+        Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g
     | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
         let
           val (v, g') = dest_abs_eta g;
-        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
+        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
         Const (@{const_syntax return}, dummyT) $ f
     | unfold_monad f = f;
@@ -164,14 +164,17 @@
     | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
         contains_bindM t;
   fun bindM_monad_tr' (f::g::ts) = list_comb
-    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
-  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb
-      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
+    (Const (@{syntax_const "_do"}, dummyT) $
+      unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
+  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
+    if contains_bindM g' then list_comb
+      (Const (@{syntax_const "_do"}, dummyT) $
+        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
     else raise Match;
-in [
-  (@{const_syntax bindM}, bindM_monad_tr'),
-  (@{const_syntax Let}, Let_monad_tr')
-] end;
+in
+ [(@{const_syntax bindM}, bindM_monad_tr'),
+  (@{const_syntax Let}, Let_monad_tr')]
+end;
 *}
 
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Inductive.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -301,10 +301,9 @@
   fun fun_tr ctxt [cs] =
     let
       val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
-      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr
-                 ctxt [x, cs]
+      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
     in lambda x ft end
-in [("_lam_pats_syntax", fun_tr)] end
+in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
 *}
 
 end
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Isar_Examples/Hoare.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -237,9 +237,9 @@
 
 parse_translation {*
   let
-    fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
+    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
       | quote_tr ts = raise TERM ("quote_tr", ts);
-  in [("_quote", quote_tr)] end
+  in [(@{syntax_const "_quote"}, quote_tr)] end
 *}
 
 text {*
@@ -251,12 +251,12 @@
 print_translation {*
   let
     fun quote_tr' f (t :: ts) =
-          Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
+          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | quote_tr' _ _ = raise Match;
 
-    val assert_tr' = quote_tr' (Syntax.const "_Assert");
+    val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
 
-    fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
+    fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
@@ -266,7 +266,7 @@
       | NONE => raise Match);
 
     fun update_name_tr' (Free x) = Free (upd_tr' x)
-      | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
+      | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
           c $ Free (upd_tr' x)
       | update_name_tr' (Const x) = Const (upd_tr' x)
       | update_name_tr' _ = raise Match;
@@ -276,12 +276,14 @@
       | K_tr' _ = raise Match;
 
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
+          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f)
             (Abs (x, dummyT, K_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
-    [("Collect", assert_tr'), ("Basic", assign_tr'),
-      ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]
+   [(@{const_syntax Collect}, assert_tr'),
+    (@{const_syntax Basic}, assign_tr'),
+    (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
+    (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"})]
   end
 *}
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Library/Coinductive_List.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -204,7 +204,7 @@
   LNil :: logic
   LCons :: logic
 translations
-  "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
+  "case p of XCONST LNil \<Rightarrow> a | XCONST LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
 
 lemma llist_case_LNil [simp, code]: "llist_case c d LNil = c"
   by (simp add: llist_case_def LNil_def
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Library/Numeral_Type.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -36,8 +36,8 @@
 
 typed_print_translation {*
 let
-  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] =
-    Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
+  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
+    Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
 in [(@{const_syntax card}, card_univ_tr')]
 end
 *}
@@ -389,7 +389,7 @@
 
 parse_translation {*
 let
-
+(* FIXME @{type_syntax} *)
 val num1_const = Syntax.const "Numeral_Type.num1";
 val num0_const = Syntax.const "Numeral_Type.num0";
 val B0_const = Syntax.const "Numeral_Type.bit0";
@@ -411,7 +411,7 @@
       mk_bintype (the (Int.fromString str))
   | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
 
-in [("_NumeralType", numeral_tr)] end;
+in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
 *}
 
 print_translation {*
@@ -419,6 +419,7 @@
 fun int_of [] = 0
   | int_of (b :: bs) = b + 2 * int_of bs;
 
+(* FIXME @{type_syntax} *)
 fun bin_of (Const ("num0", _)) = []
   | bin_of (Const ("num1", _)) = [1]
   | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
@@ -435,6 +436,7 @@
   end
   | bit_tr' b _ = raise Match;
 
+(* FIXME @{type_syntax} *)
 in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
 *}
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Library/OptionalSugar.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -15,7 +15,7 @@
 translations
   "n" <= "CONST of_nat n"
   "n" <= "CONST int n"
-  "n" <= "real n"
+  "n" <= "CONST real n"
   "n" <= "CONST real_of_nat n"
   "n" <= "CONST real_of_int n"
   "n" <= "CONST of_real n"
@@ -23,10 +23,10 @@
 
 (* append *)
 syntax (latex output)
-  "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
+  "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
 translations
-  "appendL xs ys" <= "xs @ ys" 
-  "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
+  "_appendL xs ys" <= "xs @ ys" 
+  "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
 
 
 (* deprecated, use thm with style instead, will be removed *)
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Library/State_Monad.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -159,15 +159,15 @@
   fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
         let
           val (v, g') = dest_abs_eta g;
-        in Const ("_scomp", dummyT) $ v $ f $ unfold_monad g' end
+        in Const (@{syntax_const "_scomp"}, dummyT) $ v $ f $ unfold_monad g' end
     | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
-        Const ("_fcomp", dummyT) $ f $ unfold_monad g
+        Const (@{syntax_const "_fcomp"}, dummyT) $ f $ unfold_monad g
     | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
         let
           val (v, g') = dest_abs_eta g;
-        in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
+        in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
     | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
-        Const ("return", dummyT) $ f
+        Const (@{const_syntax "return"}, dummyT) $ f
     | unfold_monad f = f;
   fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
     | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
@@ -175,18 +175,23 @@
     | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
         contains_scomp t;
   fun scomp_monad_tr' (f::g::ts) = list_comb
-    (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
-  fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb
-      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
+    (Const (@{syntax_const "_do"}, dummyT) $
+      unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
+  fun fcomp_monad_tr' (f::g::ts) =
+    if contains_scomp g then list_comb
+      (Const (@{syntax_const "_do"}, dummyT) $
+        unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
     else raise Match;
-  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb
-      (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
+  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
+    if contains_scomp g' then list_comb
+      (Const (@{syntax_const "_do"}, dummyT) $
+        unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
     else raise Match;
-in [
-  (@{const_syntax scomp}, scomp_monad_tr'),
+in
+ [(@{const_syntax scomp}, scomp_monad_tr'),
   (@{const_syntax fcomp}, fcomp_monad_tr'),
-  (@{const_syntax Let}, Let_monad_tr')
-] end;
+  (@{const_syntax Let}, Let_monad_tr')]
+end;
 *}
 
 text {*
diff -r 724e8f77806a -r b271a8996f26 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/List.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -15,13 +15,14 @@
 
 syntax
   -- {* list Enumeration *}
-  "@list" :: "args => 'a list"    ("[(_)]")
+  "_list" :: "args => 'a list"    ("[(_)]")
 
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
 
-subsection{*Basic list processing functions*}
+
+subsection {* Basic list processing functions *}
 
 primrec
   hd :: "'a list \<Rightarrow> 'a" where
@@ -68,15 +69,15 @@
 
 syntax
   -- {* Special syntax for filter *}
-  "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
+  "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
 
 translations
   "[x<-xs . P]"== "CONST filter (%x. P) xs"
 
 syntax (xsymbols)
-  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
+  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
 syntax (HTML output)
-  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
+  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
 
 primrec
   foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
@@ -132,7 +133,7 @@
   "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)
 
 translations
-  "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
+  "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
   "xs[i:=x]" == "CONST list_update xs i x"
 
 primrec
@@ -363,45 +364,52 @@
   val mapC = Syntax.const @{const_name map};
   val concatC = Syntax.const @{const_name concat};
   val IfC = Syntax.const @{const_name If};
+
   fun singl x = ConsC $ x $ NilC;
 
-   fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
+  fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
     let
       val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
       val e = if opti then singl e else e;
-      val case1 = Syntax.const "_case1" $ p $ e;
-      val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
-                                        $ NilC;
-      val cs = Syntax.const "_case2" $ case1 $ case2
-      val ft = Datatype_Case.case_tr false Datatype.info_of_constr
-                 ctxt [x, cs]
+      val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
+      val case2 = Syntax.const @{syntax_const "_case1"} $ Syntax.const Term.dummy_patternN $ NilC;
+      val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
+      val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
     in lambda x ft end;
 
   fun abs_tr ctxt (p as Free(s,T)) e opti =
-        let val thy = ProofContext.theory_of ctxt;
-            val s' = Sign.intern_const thy s
-        in if Sign.declared_const thy s'
-           then (pat_tr ctxt p e opti, false)
-           else (lambda p e, true)
+        let
+          val thy = ProofContext.theory_of ctxt;
+          val s' = Sign.intern_const thy s;
+        in
+          if Sign.declared_const thy s'
+          then (pat_tr ctxt p e opti, false)
+          else (lambda p e, true)
         end
     | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
 
-  fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =
-        let val res = case qs of Const("_lc_end",_) => singl e
-                      | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];
+  fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
+        let
+          val res =
+            (case qs of
+              Const (@{syntax_const "_lc_end"}, _) => singl e
+            | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
         in IfC $ b $ res $ NilC end
-    | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] =
+    | lc_tr ctxt
+          [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
+            Const(@{syntax_const "_lc_end"}, _)] =
         (case abs_tr ctxt p e true of
-           (f,true) => mapC $ f $ es
-         | (f, false) => concatC $ (mapC $ f $ es))
-    | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] =
-        let val e' = lc_tr ctxt [e,q,qs];
-        in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end
-
-in [("_listcompr", lc_tr)] end
+          (f, true) => mapC $ f $ es
+        | (f, false) => concatC $ (mapC $ f $ es))
+    | lc_tr ctxt
+          [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
+            Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
+        let val e' = lc_tr ctxt [e, q, qs];
+        in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
+
+in [(@{syntax_const "_listcompr"}, lc_tr)] end
 *}
 
-(*
 term "[(x,y,z). b]"
 term "[(x,y,z). x\<leftarrow>xs]"
 term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
@@ -418,9 +426,11 @@
 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
+(*
 term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
 *)
 
+
 subsubsection {* @{const Nil} and @{const Cons} *}
 
 lemma not_Cons_self [simp]:
@@ -1019,6 +1029,7 @@
   "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
   by (induct xs) auto
 
+
 subsubsection {* @{text filter} *}
 
 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
@@ -1200,6 +1211,7 @@
 
 declare partition.simps[simp del]
 
+
 subsubsection {* @{text concat} *}
 
 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
@@ -2074,6 +2086,7 @@
   qed simp
 qed simp
 
+
 subsubsection {* @{text list_all2} *}
 
 lemma list_all2_lengthD [intro?]: 
@@ -2413,6 +2426,7 @@
   unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
     by (simp add: sup_commute)
 
+
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
 
 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
@@ -2835,6 +2849,7 @@
   from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
 qed
 
+
 subsubsection {* @{const insert} *}
 
 lemma in_set_insert [simp]:
@@ -3254,7 +3269,8 @@
  apply auto
 done
 
-subsubsection{*Transpose*}
+
+subsubsection {* Transpose *}
 
 function transpose where
 "transpose []             = []" |
@@ -3366,6 +3382,7 @@
     by (simp add: nth_transpose filter_map comp_def)
 qed
 
+
 subsubsection {* (In)finiteness *}
 
 lemma finite_maxlen:
@@ -3407,7 +3424,7 @@
 done
 
 
-subsection {*Sorting*}
+subsection {* Sorting *}
 
 text{* Currently it is not shown that @{const sort} returns a
 permutation of its input because the nicest proof is via multisets,
@@ -3626,7 +3643,8 @@
 apply(simp add:sorted_Cons)
 done
 
-subsubsection {*@{const transpose} on sorted lists*}
+
+subsubsection {* @{const transpose} on sorted lists *}
 
 lemma sorted_transpose[simp]:
   shows "sorted (rev (map length (transpose xs)))"
@@ -3774,6 +3792,7 @@
     by (auto simp: nth_transpose intro: nth_equalityI)
 qed
 
+
 subsubsection {* @{text sorted_list_of_set} *}
 
 text{* This function maps (finite) linearly ordered sets to sorted
@@ -3805,6 +3824,7 @@
 
 end
 
+
 subsubsection {* @{text lists}: the list-forming operator over sets *}
 
 inductive_set
@@ -3864,8 +3884,7 @@
 by auto
 
 
-
-subsubsection{* Inductive definition for membership *}
+subsubsection {* Inductive definition for membership *}
 
 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
 where
@@ -3881,8 +3900,7 @@
 done
 
 
-
-subsubsection{*Lists as Cartesian products*}
+subsubsection {* Lists as Cartesian products *}
 
 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
 @{term A} and tail drawn from @{term Xs}.*}
@@ -3903,7 +3921,7 @@
   |  "listset (A # As) = set_Cons A (listset As)"
 
 
-subsection{*Relations on Lists*}
+subsection {* Relations on Lists *}
 
 subsubsection {* Length Lexicographic Ordering *}
 
@@ -4108,7 +4126,7 @@
 by auto
 
 
-subsubsection{*Lifting a Relation on List Elements to the Lists*}
+subsubsection {* Lifting a Relation on List Elements to the Lists *}
 
 inductive_set
   listrel :: "('a * 'a)set => ('a list * 'a list)set"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Map.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -68,7 +68,7 @@
 
 translations
   "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
-  "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
+  "_MapUpd m (_maplet  x y)"    == "m(x := CONST Some y)"
   "_Map ms"                     == "_MapUpd (CONST empty) ms"
   "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
   "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Metis_Examples/Message.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -45,10 +45,10 @@
 
 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
 syntax
-  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
+  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
 
 syntax (xsymbols)
-  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
 
 translations
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/MicroJava/DFA/Product.thy
--- a/src/HOL/MicroJava/DFA/Product.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/MicroJava/DFA/Product.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -19,9 +19,10 @@
  esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
 "esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
 
-syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
+abbreviation
+  lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool"
        ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
-translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
+  where "p <=(rA,rB) q == p <=_(le rA rB) q"
 
 lemma unfold_lesub_prod:
   "p <=(rA,rB) q == le rA rB p q"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -33,9 +33,9 @@
   "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
 (*<*)
  (* allow \<sub> instead of \<bsub>..\<esub> *)  
-  "@lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
-  "@lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
-  "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+  "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
+  "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
+  "_plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
 
 translations
   "x \<sqsubseteq>\<^sub>r y" => "x \<sqsubseteq>\<^bsub>r\<^esub> y"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/MicroJava/DFA/SemilatAlg.thy
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -15,7 +15,7 @@
   "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
 
 consts
- "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
+  plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
 primrec
   "[] ++_f y = y"
   "(x#xs) ++_f y = xs ++_f (x +_f y)"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -38,7 +38,7 @@
   "_idts"       :: "[idt, idts] => idts"                ("_,/ _" [1, 0] 0)
 
   "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1_,/ _)")
-(* "@pttrn"     :: "[pttrn, pttrns] => pttrn"           ("_,/ _" [1, 0] 0)
+(* "_pttrn"     :: "[pttrn, pttrns] => pttrn"           ("_,/ _" [1, 0] 0)
   "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/ _" [1, 0] 0) *)
 
   "_decl"       :: "[mutype,pttrn] => decl"             ("_ _")
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -27,14 +27,14 @@
 
 parse_translation {*
 let
-  fun cart t u = Syntax.const @{type_name cart} $ t $ u
+  fun cart t u = Syntax.const @{type_name cart} $ t $ u;   (* FIXME @{type_syntax} *)
   fun finite_cart_tr [t, u as Free (x, _)] =
-        if Syntax.is_tid x
-        then cart t (Syntax.const "_ofsort" $ u $ Syntax.const (hd @{sort finite}))
+        if Syntax.is_tid x then
+          cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const (hd @{sort finite}))
         else cart t u
     | finite_cart_tr [t, u] = cart t u
 in
-  [("_finite_cart", finite_cart_tr)]
+  [(@{syntax_const "_finite_cart"}, finite_cart_tr)]
 end
 *}
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Orderings.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -646,25 +646,30 @@
   val less_eq = @{const_syntax less_eq};
 
   val trans =
-   [((All_binder, impl, less), ("_All_less", "_All_greater")),
-    ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")),
-    ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")),
-    ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
+   [((All_binder, impl, less),
+    (@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})),
+    ((All_binder, impl, less_eq),
+    (@{syntax_const "_All_less_eq"}, @{syntax_const "_All_greater_eq"})),
+    ((Ex_binder, conj, less),
+    (@{syntax_const "_Ex_less"}, @{syntax_const "_Ex_greater"})),
+    ((Ex_binder, conj, less_eq),
+    (@{syntax_const "_Ex_less_eq"}, @{syntax_const "_Ex_greater_eq"}))];
 
-  fun matches_bound v t = 
-     case t of (Const ("_bound", _) $ Free (v', _)) => (v = v')
-              | _ => false
-  fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false)
-  fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P
+  fun matches_bound v t =
+    (case t of
+      Const ("_bound", _) $ Free (v', _) => v = v'
+    | _ => false);
+  fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
+  fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
 
   fun tr' q = (q,
     fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
-      (case AList.lookup (op =) trans (q, c, d) of
-        NONE => raise Match
-      | SOME (l, g) =>
-          if matches_bound v t andalso not (contains_var v u) then mk v l u P
-          else if matches_bound v u andalso not (contains_var v t) then mk v g t P
-          else raise Match)
+        (case AList.lookup (op =) trans (q, c, d) of
+          NONE => raise Match
+        | SOME (l, g) =>
+            if matches_bound v t andalso not (contains_var v u) then mk v l u P
+            else if matches_bound v u andalso not (contains_var v t) then mk v g t P
+            else raise Match)
      | _ => raise Match);
 in [tr' All_binder, tr' Ex_binder] end
 *}
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Product_Type.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -180,65 +180,81 @@
   "_patterns"   :: "[pttrn, patterns] => patterns"      ("_,/ _")
 
 translations
-  "(x, y)"       == "Pair x y"
+  "(x, y)" == "CONST Pair x y"
   "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
-  "%(x,y,zs).b"  == "split(%x (y,zs).b)"
-  "%(x,y).b"     == "split(%x y. b)"
-  "_abs (Pair x y) t" => "%(x,y).t"
+  "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
+  "%(x, y). b" == "CONST split (%x y. b)"
+  "_abs (CONST Pair x y) t" => "%(x, y). t"
   (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
 
-(* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)
-(* works best with enclosing "let", if "let" does not avoid eta-contraction   *)
+(*reconstruct pattern from (nested) splits, avoiding eta-contraction of body;
+  works best with enclosing "let", if "let" does not avoid eta-contraction*)
 print_translation {*
-let fun split_tr' [Abs (x,T,t as (Abs abs))] =
-      (* split (%x y. t) => %(x,y) t *)
-      let val (y,t') = atomic_abs_tr' abs;
-          val (x',t'') = atomic_abs_tr' (x,T,t');
-    
-      in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end
-    | split_tr' [Abs (x,T,(s as Const ("split",_)$t))] =
-       (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
-       let val (Const ("_abs",_)$(Const ("_pattern",_)$y$z)$t') = split_tr' [t];
-           val (x',t'') = atomic_abs_tr' (x,T,t');
-       in Syntax.const "_abs"$ 
-           (Syntax.const "_pattern"$x'$(Syntax.const "_patterns"$y$z))$t'' end
-    | split_tr' [Const ("split",_)$t] =
-       (* split (split (%x y z. t)) => %((x,y),z). t *)   
-       split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
-    | split_tr' [Const ("_abs",_)$x_y$(Abs abs)] =
-       (* split (%pttrn z. t) => %(pttrn,z). t *)
-       let val (z,t) = atomic_abs_tr' abs;
-       in Syntax.const "_abs" $ (Syntax.const "_pattern" $x_y$z) $ t end
-    | split_tr' _ =  raise Match;
-in [("split", split_tr')]
-end
+let
+  fun split_tr' [Abs (x, T, t as (Abs abs))] =
+        (* split (%x y. t) => %(x,y) t *)
+        let
+          val (y, t') = atomic_abs_tr' abs;
+          val (x', t'') = atomic_abs_tr' (x, T, t');
+        in
+          Syntax.const @{syntax_const "_abs"} $
+            (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+        end
+    | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] =
+        (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
+        let
+          val Const (@{syntax_const "_abs"}, _) $
+            (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
+          val (x', t'') = atomic_abs_tr' (x, T, t');
+        in
+          Syntax.const @{syntax_const "_abs"} $
+            (Syntax.const @{syntax_const "_pattern"} $ x' $
+              (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
+        end
+    | split_tr' [Const (@{const_syntax split}, _) $ t] =
+        (* split (split (%x y z. t)) => %((x, y), z). t *)
+        split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
+    | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
+        (* split (%pttrn z. t) => %(pttrn,z). t *)
+        let val (z, t) = atomic_abs_tr' abs in
+          Syntax.const @{syntax_const "_abs"} $
+            (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
+        end
+    | split_tr' _ = raise Match;
+in [(@{const_syntax split}, split_tr')] end
 *}
 
 (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
 typed_print_translation {*
 let
-  fun split_guess_names_tr' _ T [Abs (x,_,Abs _)] = raise Match
-    | split_guess_names_tr' _ T  [Abs (x,xT,t)] =
+  fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
+    | split_guess_names_tr' _ T [Abs (x, xT, t)] =
         (case (head_of t) of
-           Const ("split",_) => raise Match
-         | _ => let 
-                  val (_::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
-                  val (y,t') = atomic_abs_tr' ("y",yT,(incr_boundvars 1 t)$Bound 0); 
-                  val (x',t'') = atomic_abs_tr' (x,xT,t');
-                in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
+          Const (@{const_syntax split}, _) => raise Match
+        | _ =>
+          let 
+            val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
+            val (x', t'') = atomic_abs_tr' (x, xT, t');
+          in
+            Syntax.const @{syntax_const "_abs"} $
+              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+          end)
     | split_guess_names_tr' _ T [t] =
-       (case (head_of t) of
-           Const ("split",_) => raise Match 
-         | _ => let 
-                  val (xT::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
-                  val (y,t') = 
-                        atomic_abs_tr' ("y",yT,(incr_boundvars 2 t)$Bound 1$Bound 0); 
-                  val (x',t'') = atomic_abs_tr' ("x",xT,t');
-                in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
+        (case head_of t of
+          Const (@{const_syntax split}, _) => raise Match
+        | _ =>
+          let
+            val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+            val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
+            val (x', t'') = atomic_abs_tr' ("x", xT, t');
+          in
+            Syntax.const @{syntax_const "_abs"} $
+              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+          end)
     | split_guess_names_tr' _ _ _ = raise Match;
-in [("split", split_guess_names_tr')]
-end 
+in [(@{const_syntax split}, split_guess_names_tr')] end
 *}
 
 
@@ -855,10 +871,9 @@
   Times  (infixr "\<times>" 80)
 
 syntax
-  "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
-
+  "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
 translations
-  "SIGMA x:A. B" == "Product_Type.Sigma A (%x. B)"
+  "SIGMA x:A. B" == "CONST Sigma A (%x. B)"
 
 lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   by (unfold Sigma_def) blast
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Prolog/Test.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -18,7 +18,7 @@
 
 syntax
   (* list Enumeration *)
-  "@list"     :: "args => 'a list"                          ("[(_)]")
+  "_list"     :: "args => 'a list"                          ("[(_)]")
 
 translations
   "[x, xs]"     == "x#[xs]"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Set.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -48,20 +48,16 @@
 text {* Set comprehensions *}
 
 syntax
-  "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
-
+  "_Coll" :: "pttrn => bool => 'a set"    ("(1{_./ _})")
 translations
-  "{x. P}"      == "Collect (%x. P)"
+  "{x. P}" == "CONST Collect (%x. P)"
 
 syntax
-  "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
-  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
-
+  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
 syntax (xsymbols)
-  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
-
+  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
 translations
-  "{x:A. P}"    => "{x. x:A & P}"
+  "{x:A. P}" => "{x. x:A & P}"
 
 lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
   by (simp add: Collect_def mem_def)
@@ -107,11 +103,10 @@
   insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
 syntax
-  "@Finset"     :: "args => 'a set"                       ("{(_)}")
-
+  "_Finset" :: "args => 'a set"    ("{(_)}")
 translations
-  "{x, xs}"     == "CONST insert x {xs}"
-  "{x}"         == "CONST insert x {}"
+  "{x, xs}" == "CONST insert x {xs}"
+  "{x}" == "CONST insert x {}"
 
 
 subsection {* Subsets and bounded quantifiers *}
@@ -191,9 +186,9 @@
   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
 
 translations
-  "ALL x:A. P"  == "Ball A (%x. P)"
-  "EX x:A. P"   == "Bex A (%x. P)"
-  "EX! x:A. P"  => "EX! x. x:A & P"
+  "ALL x:A. P" == "CONST Ball A (%x. P)"
+  "EX x:A. P" == "CONST Bex A (%x. P)"
+  "EX! x:A. P" => "EX! x. x:A & P"
   "LEAST x:A. P" => "LEAST x. x:A & P"
 
 syntax (output)
@@ -233,31 +228,34 @@
 
 print_translation {*
 let
-  val Type (set_type, _) = @{typ "'a set"};
-  val All_binder = Syntax.binder_name @{const_syntax "All"};
-  val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
+  val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
+  val All_binder = Syntax.binder_name @{const_syntax All};
+  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
   val impl = @{const_syntax "op -->"};
   val conj = @{const_syntax "op &"};
-  val sbset = @{const_syntax "subset"};
-  val sbset_eq = @{const_syntax "subset_eq"};
+  val sbset = @{const_syntax subset};
+  val sbset_eq = @{const_syntax subset_eq};
 
   val trans =
-   [((All_binder, impl, sbset), "_setlessAll"),
-    ((All_binder, impl, sbset_eq), "_setleAll"),
-    ((Ex_binder, conj, sbset), "_setlessEx"),
-    ((Ex_binder, conj, sbset_eq), "_setleEx")];
+   [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
+    ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
+    ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
+    ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
 
   fun mk v v' c n P =
     if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
     then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
 
   fun tr' q = (q,
-    fn [Const ("_bound", _) $ Free (v, Type (T, _)), Const (c, _) $ (Const (d, _) $ (Const ("_bound", _) $ Free (v', _)) $ n) $ P] =>
-         if T = (set_type) then case AList.lookup (op =) trans (q, c, d)
-          of NONE => raise Match
-           | SOME l => mk v v' l n P
-         else raise Match
-     | _ => raise Match);
+        fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)),
+            Const (c, _) $
+              (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', _)) $ n) $ P] =>
+            if T = set_type then
+              (case AList.lookup (op =) trans (q, c, d) of
+                NONE => raise Match
+              | SOME l => mk v v' l n P)
+            else raise Match
+         | _ => raise Match);
 in
   [tr' All_binder, tr' Ex_binder]
 end
@@ -270,55 +268,63 @@
   only translated if @{text "[0..n] subset bvs(e)"}.
 *}
 
+syntax
+  "_Setcompr" :: "'a => idts => bool => 'a set"    ("(1{_ |/_./ _})")
+
 parse_translation {*
   let
-    val ex_tr = snd (mk_binder_tr ("EX ", "Ex"));
+    val ex_tr = snd (mk_binder_tr ("EX ", @{const_syntax Ex}));
 
-    fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1
+    fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
       | nvars _ = 1;
 
     fun setcompr_tr [e, idts, b] =
       let
-        val eq = Syntax.const "op =" $ Bound (nvars idts) $ e;
-        val P = Syntax.const "op &" $ eq $ b;
+        val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
+        val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
         val exP = ex_tr [idts, P];
-      in Syntax.const "Collect" $ Term.absdummy (dummyT, exP) end;
+      in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
 
-  in [("@SetCompr", setcompr_tr)] end;
+  in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
 *}
 
-print_translation {* [
-Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} "_Ball",
-Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} "_Bex"
-] *} -- {* to avoid eta-contraction of body *}
+print_translation {*
+ [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
+  Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
+*} -- {* to avoid eta-contraction of body *}
 
 print_translation {*
 let
-  val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
+  val ex_tr' = snd (mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
 
   fun setcompr_tr' [Abs (abs as (_, _, P))] =
     let
-      fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
-        | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
+      fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
+        | check (Const (@{const_syntax "op &"}, _) $
+              (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
             n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
             subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
-        | check _ = false
+        | check _ = false;
 
         fun tr' (_ $ abs) =
           let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
-          in Syntax.const "@SetCompr" $ e $ idts $ Q end;
-    in if check (P, 0) then tr' P
-       else let val (x as _ $ Free(xN,_), t) = atomic_abs_tr' abs
-                val M = Syntax.const "@Coll" $ x $ t
-            in case t of
-                 Const("op &",_)
-                   $ (Const("op :",_) $ (Const("_bound",_) $ Free(yN,_)) $ A)
-                   $ P =>
-                   if xN=yN then Syntax.const "@Collect" $ x $ A $ P else M
-               | _ => M
-            end
+          in Syntax.const @{syntax_const "_Setcompr"} $ e $ idts $ Q end;
+    in
+      if check (P, 0) then tr' P
+      else
+        let
+          val (x as _ $ Free(xN, _), t) = atomic_abs_tr' abs;
+          val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
+        in
+          case t of
+            Const (@{const_syntax "op &"}, _) $
+              (Const (@{const_syntax "op :"}, _) $
+                (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
+            if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
+          | _ => M
+        end
     end;
-  in [("Collect", setcompr_tr')] end;
+  in [(@{const_syntax Collect}, setcompr_tr')] end;
 *}
 
 setup {*
diff -r 724e8f77806a -r b271a8996f26 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/SetInterval.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -54,22 +54,22 @@
 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
 
 syntax
-  "@UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
-  "@UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
-  "@INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
-  "@INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
 
 syntax (xsymbols)
-  "@UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
-  "@UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
-  "@INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
-  "@INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
 
 syntax (latex output)
-  "@UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
-  "@UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
-  "@INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
-  "@INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
+  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
+  "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
+  "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
+  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
 
 translations
   "UN i<=n. A"  == "UN i:{..n}. A"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Statespace/StateFun.thy
--- a/src/HOL/Statespace/StateFun.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Statespace/StateFun.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      StateFun.thy
-    ID:         $Id$
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -34,12 +33,12 @@
 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
   by (rule refl)
 
-constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
-"lookup destr n s \<equiv> destr (s n)"
+definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
+  where "lookup destr n s = destr (s n)"
 
-constdefs update:: 
+definition update::
   "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
-"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
+  where "update destr constr n f s = s(n := constr (f (destr (s n))))"
 
 lemma lookup_update_same:
   "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) = 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Statespace/StateSpaceSyntax.thy
--- a/src/HOL/Statespace/StateSpaceSyntax.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      StateSpaceSyntax.thy
-    ID:         $Id$
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -13,30 +12,27 @@
 can choose if you want to use it or not.  *}
 
 syntax 
- "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60,60] 60)
- "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
- "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900,0] 900)
+  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
+  "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
+  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  ("_<_>" [900, 0] 900)
 
 translations
-  "_statespace_updates f (_updbinds b bs)"  == 
-     "_statespace_updates (_statespace_updates f b) bs"
-  "s<x:=y>"                     == "_statespace_update s x y"
+  "_statespace_updates f (_updbinds b bs)" ==
+    "_statespace_updates (_statespace_updates f b) bs"
+  "s<x:=y>" == "_statespace_update s x y"
 
 
 parse_translation (advanced)
 {*
-[("_statespace_lookup",StateSpace.lookup_tr),
- ("_get",StateSpace.lookup_tr),
- ("_statespace_update",StateSpace.update_tr)] 
+ [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
+  (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
 *}
 
 
 print_translation (advanced)
 {*
-[("lookup",StateSpace.lookup_tr'),
- ("StateFun.lookup",StateSpace.lookup_tr'),
- ("update",StateSpace.update_tr'),
- ("StateFun.update",StateSpace.update_tr')] 
+ [(@{const_syntax lookup}, StateSpace.lookup_tr'),
+  (@{const_syntax update}, StateSpace.update_tr')]
 *}
 
-end
\ No newline at end of file
+end
diff -r 724e8f77806a -r b271a8996f26 src/HOL/String.thy
--- a/src/HOL/String.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/String.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -5,7 +5,7 @@
 theory String
 imports List
 uses
-  "Tools/string_syntax.ML"
+  ("Tools/string_syntax.ML")
   ("Tools/string_code.ML")
 begin
 
@@ -78,6 +78,7 @@
 syntax
   "_String" :: "xstr => string"    ("_")
 
+use "Tools/string_syntax.ML"
 setup StringSyntax.setup
 
 definition chars :: string where
diff -r 724e8f77806a -r b271a8996f26 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/Action.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,8 +1,6 @@
-(*
-    File:        TLA/Action.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/Action.thy 
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 *)
 
 header {* The action level of TLA as an Isabelle theory *}
@@ -50,13 +48,13 @@
 
 translations
   "ACT A"            =>   "(A::state*state => _)"
-  "_before"          ==   "before"
-  "_after"           ==   "after"
+  "_before"          ==   "CONST before"
+  "_after"           ==   "CONST after"
   "_prime"           =>   "_after"
-  "_unchanged"       ==   "unch"
-  "_SqAct"           ==   "SqAct"
-  "_AnAct"           ==   "AnAct"
-  "_Enabled"         ==   "enabled"
+  "_unchanged"       ==   "CONST unch"
+  "_SqAct"           ==   "CONST SqAct"
+  "_AnAct"           ==   "CONST AnAct"
+  "_Enabled"         ==   "CONST enabled"
   "w |= [A]_v"       <=   "_SqAct A v w"
   "w |= <A>_v"       <=   "_AnAct A v w"
   "s |= Enabled A"   <=   "_Enabled A s"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/TLA/Init.thy
--- a/src/HOL/TLA/Init.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/Init.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,11 +1,10 @@
-(*
-    File:        TLA/Init.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/Init.thy
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 
-Introduces type of temporal formulas. Defines interface between
-temporal formulas and its "subformulas" (state predicates and actions).
+Introduces type of temporal formulas.  Defines interface between
+temporal formulas and its "subformulas" (state predicates and
+actions).
 *)
 
 theory Init
@@ -26,12 +25,12 @@
   st2         :: "behavior => state"
 
 syntax
-  TEMP       :: "lift => 'a"                          ("(TEMP _)")
+  "_TEMP"    :: "lift => 'a"                          ("(TEMP _)")
   "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
 
 translations
   "TEMP F"   => "(F::behavior => _)"
-  "_Init"    == "Initial"
+  "_Init"    == "CONST Initial"
   "sigma |= Init F"  <= "_Init F sigma"
 
 defs
diff -r 724e8f77806a -r b271a8996f26 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/Intensional.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,8 +1,6 @@
-(*
-    File:        TLA/Intensional.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/Intensional.thy
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 *)
 
 header {* A framework for "intensional" (possible-world based) logics
@@ -95,11 +93,11 @@
   "_REx1" :: "[idts, lift] => lift"                      ("(3EX! _./ _)" [0, 10] 10)
 
 translations
-  "_const"        == "const"
-  "_lift"         == "lift"
-  "_lift2"        == "lift2"
-  "_lift3"        == "lift3"
-  "_Valid"        == "Valid"
+  "_const"        == "CONST const"
+  "_lift"         == "CONST lift"
+  "_lift2"        == "CONST lift2"
+  "_lift3"        == "CONST lift3"
+  "_Valid"        == "CONST Valid"
   "_RAll x A"     == "Rall x. A"
   "_REx x  A"     == "Rex x. A"
   "_REx1 x  A"    == "Rex! x. A"
@@ -112,11 +110,11 @@
 
   "_liftEqu"      == "_lift2 (op =)"
   "_liftNeq u v"  == "_liftNot (_liftEqu u v)"
-  "_liftNot"      == "_lift Not"
+  "_liftNot"      == "_lift (CONST Not)"
   "_liftAnd"      == "_lift2 (op &)"
   "_liftOr"       == "_lift2 (op | )"
   "_liftImp"      == "_lift2 (op -->)"
-  "_liftIf"       == "_lift3 If"
+  "_liftIf"       == "_lift3 (CONST If)"
   "_liftPlus"     == "_lift2 (op +)"
   "_liftMinus"    == "_lift2 (op -)"
   "_liftTimes"    == "_lift2 (op *)"
@@ -126,12 +124,12 @@
   "_liftLeq"      == "_lift2 (op <=)"
   "_liftMem"      == "_lift2 (op :)"
   "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
-  "_liftFinset (_liftargs x xs)"  == "_lift2 CONST insert x (_liftFinset xs)"
-  "_liftFinset x" == "_lift2 CONST insert x (_const {})"
+  "_liftFinset (_liftargs x xs)"  == "_lift2 (CONST insert) x (_liftFinset xs)"
+  "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
   "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
-  "_liftPair"     == "_lift2 Pair"
-  "_liftCons"     == "lift2 Cons"
-  "_liftApp"      == "lift2 (op @)"
+  "_liftPair"     == "_lift2 (CONST Pair)"
+  "_liftCons"     == "CONST lift2 (CONST Cons)"
+  "_liftApp"      == "CONST lift2 (op @)"
   "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
   "_liftList x"   == "_liftCons x (_const [])"
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/TLA/ROOT.ML
--- a/src/HOL/TLA/ROOT.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/ROOT.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -1,7 +1,3 @@
-(*  Title:      HOL/TLA/ROOT.ML
-
-Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
-*)
+(* The Temporal Logic of Actions *)
 
 use_thys ["TLA"];
-
diff -r 724e8f77806a -r b271a8996f26 src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/Stfun.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,8 +1,6 @@
-(*
-    File:        TLA/Stfun.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/Stfun.thy
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 *)
 
 header {* States and state functions for TLA as an "intensional" logic *}
@@ -42,7 +40,7 @@
 
 translations
   "PRED P"   =>  "(P::state => _)"
-  "_stvars"  ==  "stvars"
+  "_stvars"  ==  "CONST stvars"
 
 defs
   (* Base variables may be assigned arbitrary (type-correct) values.
diff -r 724e8f77806a -r b271a8996f26 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/TLA.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,8 +1,6 @@
-(*
-    File:        TLA/TLA.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1998 University of Munich
+(*  Title:      HOL/TLA/TLA.thy
+    Author:     Stephan Merz
+    Copyright:  1998 University of Munich
 *)
 
 header {* The temporal level of TLA *}
@@ -1168,4 +1166,3 @@
   done
 
 end
-
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Tools/float_syntax.ML
--- a/src/HOL/Tools/float_syntax.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Tools/float_syntax.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -1,7 +1,6 @@
-(*  ID:         $Id$
-    Authors:    Tobias Nipkow, TU Muenchen
+(*  Author:     Tobias Nipkow, TU Muenchen
 
-Concrete syntax for floats
+Concrete syntax for floats.
 *)
 
 signature FLOAT_SYNTAX =
@@ -18,19 +17,21 @@
 
 fun mk_number i =
   let
-    fun mk 0 = Syntax.const @{const_name Int.Pls}
-      | mk ~1 =  Syntax.const @{const_name Int.Min}
-      | mk i = let val (q, r) = Integer.div_mod i 2
-               in HOLogic.mk_bit r $ (mk q) end;
-  in Syntax.const @{const_name Int.number_of} $ mk i end;
+    fun mk 0 = Syntax.const @{const_syntax Int.Pls}
+      | mk ~1 = Syntax.const @{const_syntax Int.Min}
+      | mk i =
+          let val (q, r) = Integer.div_mod i 2
+          in HOLogic.mk_bit r $ (mk q) end;
+  in Syntax.const @{const_syntax Int.number_of} $ mk i end;
 
 fun mk_frac str =
   let
-    val {mant=i, exp = n} = Syntax.read_float str;
-    val exp = Syntax.const @{const_name Power.power};
+    val {mant = i, exp = n} = Syntax.read_float str;
+    val exp = Syntax.const @{const_syntax Power.power};
     val ten = mk_number 10;
-    val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
-  in (Syntax.const @{const_name divide}) $ (mk_number i) $ exp10 end
+    val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
+  in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
+
 in
 
 fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
@@ -42,6 +43,6 @@
 (* theory setup *)
 
 val setup =
-  Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
+  Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
 
 end;
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Tools/numeral_syntax.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -27,7 +27,7 @@
 in
 
 fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
-      Syntax.const @{const_name Int.number_of} $ mk_bin num
+      Syntax.const @{const_syntax Int.number_of} $ mk_bin num
   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
 
 end;
@@ -37,10 +37,10 @@
 
 local
 
-fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
-  | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
-  | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
-  | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
+fun dest_bin (Const (@{const_syntax Int.Pls}, _)) = []
+  | dest_bin (Const (@{const_syntax Int.Min}, _)) = [~1]
+  | dest_bin (Const (@{const_syntax Int.Bit0}, _) $ bs) = 0 :: dest_bin bs
+  | dest_bin (Const (@{const_syntax Int.Bit1}, _) $ bs) = 1 :: dest_bin bs
   | dest_bin _ = raise Match;
 
 fun leading _ [] = 0
@@ -64,11 +64,12 @@
   end;
 
 fun syntax_numeral t =
-  Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t));
+  Syntax.const @{syntax_const "_Numeral"} $
+    (Syntax.const @{syntax_const "_numeral"} $ Syntax.free (dest_bin_str t));
 
 in
 
-fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
+fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =  (* FIXME @{type_syntax} *)
       let val t' =
         if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
         else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
@@ -84,7 +85,7 @@
 (* theory setup *)
 
 val setup =
-  Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
+  Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
   Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
 
 end;
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Tools/string_syntax.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -30,7 +30,7 @@
 
 fun mk_char s =
   if Symbol.is_ascii s then
-    Syntax.Appl [Syntax.Constant "Char", mk_nib (ord s div 16), mk_nib (ord s mod 16)]
+    Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
   else error ("Non-ASCII symbol: " ^ quote s);
 
 val specials = explode "\\\"`'";
@@ -41,11 +41,13 @@
     then c else raise Match
   end;
 
-fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
+fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
   | dest_char _ = raise Match;
 
 fun syntax_string cs =
-  Syntax.Appl [Syntax.Constant "_inner_string", Syntax.Variable (Syntax.implode_xstr cs)];
+  Syntax.Appl
+    [Syntax.Constant @{syntax_const "_inner_string"},
+      Syntax.Variable (Syntax.implode_xstr cs)];
 
 
 fun char_ast_tr [Syntax.Variable xstr] =
@@ -54,24 +56,29 @@
     | _ => error ("Single character expected: " ^ xstr))
   | char_ast_tr asts = raise AST ("char_ast_tr", asts);
 
-fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_string [dest_chr c1 c2]]
+fun char_ast_tr' [c1, c2] =
+      Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
   | char_ast_tr' _ = raise Match;
 
 
 (* string *)
 
-fun mk_string [] = Syntax.Constant "Nil"
-  | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
+fun mk_string [] = Syntax.Constant @{const_syntax Nil}
+  | mk_string (c :: cs) =
+      Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
 
 fun string_ast_tr [Syntax.Variable xstr] =
     (case Syntax.explode_xstr xstr of
-      [] => Syntax.Appl
-        [Syntax.Constant Syntax.constrainC, Syntax.Constant "Nil", Syntax.Constant "string"]
+      [] =>
+        Syntax.Appl
+          [Syntax.Constant Syntax.constrainC,
+            Syntax.Constant @{const_syntax Nil}, Syntax.Constant "string"]  (* FIXME @{type_syntax} *)
     | cs => mk_string cs)
   | string_ast_tr asts = raise AST ("string_tr", asts);
 
-fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
-        syntax_string (map dest_char (Syntax.unfold_ast "_args" args))]
+fun list_ast_tr' [args] =
+      Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
+        syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
   | list_ast_tr' ts = raise Match;
 
 
@@ -79,7 +86,7 @@
 
 val setup =
   Sign.add_trfuns
-    ([("_Char", char_ast_tr), ("_String", string_ast_tr)], [], [],
-      [("Char", char_ast_tr'), ("@list", list_ast_tr')]);
+   ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
+    [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
 
 end;
diff -r 724e8f77806a -r b271a8996f26 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Typerep.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -17,22 +17,27 @@
 
 end
 
-setup {*
+syntax
+  "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
+
+parse_translation {*
 let
   fun typerep_tr (*"_TYPEREP"*) [ty] =
-        Lexicon.const @{const_syntax typerep} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $
-          (Lexicon.const "itself" $ ty))
+        Syntax.const @{const_syntax typerep} $
+          (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
+            (Syntax.const "itself" $ ty))  (* FIXME @{type_syntax} *)
     | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
-  fun typerep_tr' show_sorts (*"typerep"*)
+in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
+*}
+
+typed_print_translation {*
+let
+  fun typerep_tr' show_sorts (*"typerep"*)  (* FIXME @{type_syntax} *)
           (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
-        Term.list_comb (Lexicon.const "_TYPEREP" $ Syntax.term_of_typ show_sorts T, ts)
+        Term.list_comb
+          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
     | typerep_tr' _ T ts = raise Match;
-in
-  Sign.add_syntax_i
-    [("_TYPEREP", Simple_Syntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
-  #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
-  #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
-end
+in [(@{const_syntax typerep}, typerep_tr')] end
 *}
 
 setup {*
diff -r 724e8f77806a -r b271a8996f26 src/HOL/ex/Antiquote.thy
--- a/src/HOL/ex/Antiquote.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/ex/Antiquote.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,11 +1,12 @@
 (*  Title:      HOL/ex/Antiquote.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Antiquotations *}
 
-theory Antiquote imports Main begin
+theory Antiquote
+imports Main
+begin
 
 text {*
   A simple example on quote / antiquote in higher-order abstract
@@ -13,17 +14,23 @@
 *}
 
 syntax
-  "_Expr" :: "'a => 'a"                         ("EXPR _" [1000] 999)
+  "_Expr" :: "'a => 'a"    ("EXPR _" [1000] 999)
 
-constdefs
-  var :: "'a => ('a => nat) => nat"             ("VAR _" [1000] 999)
-  "var x env == env x"
+definition
+  var :: "'a => ('a => nat) => nat"    ("VAR _" [1000] 999)
+  where "var x env = env x"
 
+definition
   Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
-  "Expr exp env == exp env"
+  where "Expr exp env = exp env"
 
-parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *}
-print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *}
+parse_translation {*
+  [Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
+*}
+
+print_translation {*
+  [Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
+*}
 
 term "EXPR (a + b + c)"
 term "EXPR (a + b + c + VAR x + VAR y + 1)"
diff -r 724e8f77806a -r b271a8996f26 src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/ex/Binary.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Binary.thy
-    ID:         $Id$
     Author:     Makarius
 *)
 
@@ -21,8 +20,6 @@
   unfolding bit_def by simp_all
 
 ML {*
-structure Binary =
-struct
   fun dest_bit (Const (@{const_name False}, _)) = 0
     | dest_bit (Const (@{const_name True}, _)) = 1
     | dest_bit t = raise TERM ("dest_bit", [t]);
@@ -43,7 +40,6 @@
         else
           let val (q, r) = Integer.div_mod n 2
           in @{term bit} $ mk_binary q $ mk_bit r end;
-end
 *}
 
 
@@ -126,7 +122,7 @@
   fun binary_proc proc ss ct =
     (case Thm.term_of ct of
       _ $ t $ u =>
-      (case try (pairself (`Binary.dest_binary)) (t, u) of
+      (case try (pairself (`dest_binary)) (t, u) of
         SOME args => proc (Simplifier.the_context ss) args
       | NONE => NONE)
     | _ => NONE);
@@ -135,34 +131,34 @@
 val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   let val k = n - m in
     if k >= 0 then
-      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (Binary.mk_binary k))])
+      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))])
     else
       SOME (@{thm binary_less_eq(2)} OF
-        [prove ctxt (t == plus (plus u (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
+        [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))])
   end);
 
 val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   let val k = m - n in
     if k >= 0 then
-      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
+      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))])
     else
       SOME (@{thm binary_less(2)} OF
-        [prove ctxt (u == plus (plus t (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
+        [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))])
   end);
 
 val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   let val k = m - n in
     if k >= 0 then
-      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
+      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))])
     else
-      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (Binary.mk_binary (~ k)))])
+      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))])
   end);
 
 fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   if n = 0 then NONE
   else
     let val (k, l) = Integer.div_mod m n
-    in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end);
+    in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end);
 
 end;
 *}
@@ -194,17 +190,17 @@
 
 parse_translation {*
 let
-
-val syntax_consts = map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
+  val syntax_consts =
+    map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
 
-fun binary_tr [Const (num, _)] =
-      let
-        val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
-        val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
-      in syntax_consts (Binary.mk_binary n) end
-  | binary_tr ts = raise TERM ("binary_tr", ts);
+  fun binary_tr [Const (num, _)] =
+        let
+          val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
+          val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
+        in syntax_consts (mk_binary n) end
+    | binary_tr ts = raise TERM ("binary_tr", ts);
 
-in [("_Binary", binary_tr)] end
+in [(@{syntax_const "_Binary"}, binary_tr)] end
 *}
 
 
diff -r 724e8f77806a -r b271a8996f26 src/HOL/ex/Multiquote.thy
--- a/src/HOL/ex/Multiquote.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/ex/Multiquote.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,11 +1,12 @@
 (*  Title:      HOL/ex/Multiquote.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Multiple nested quotations and anti-quotations *}
 
-theory Multiquote imports Main begin
+theory Multiquote
+imports Main
+begin
 
 text {*
   Multiple nested quotations and anti-quotations -- basically a
@@ -13,25 +14,25 @@
 *}
 
 syntax
-  "_quote" :: "'b => ('a => 'b)"             ("\<guillemotleft>_\<guillemotright>" [0] 1000)
-  "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
+  "_quote" :: "'b => ('a => 'b)"    ("\<guillemotleft>_\<guillemotright>" [0] 1000)
+  "_antiquote" :: "('a => 'b) => 'b"    ("\<acute>_" [1000] 1000)
 
 parse_translation {*
   let
-    fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
-          skip_antiquote_tr i t
-      | antiquote_tr i (Const ("_antiquote", _) $ t) =
+    fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $
+          (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t
+      | antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ t) =
           antiquote_tr i t $ Bound i
       | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
       | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
       | antiquote_tr _ a = a
-    and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
+    and skip_antiquote_tr i ((c as Const (@{syntax_const "_antiquote"}, _)) $ t) =
           c $ skip_antiquote_tr i t
       | skip_antiquote_tr i t = antiquote_tr i t;
 
     fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
       | quote_tr ts = raise TERM ("quote_tr", ts);
-  in [("_quote", quote_tr)] end
+  in [(@{syntax_const "_quote"}, quote_tr)] end
 *}
 
 text {* basic examples *}
diff -r 724e8f77806a -r b271a8996f26 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/ex/Numeral.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -311,7 +311,7 @@
             orelse error ("Bad numeral: " ^ num);
         in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
     | numeral_tr ts = raise TERM ("numeral_tr", ts);
-in [("_Numerals", numeral_tr)] end
+in [(@{syntax_const "_Numerals"}, numeral_tr)] end
 *}
 
 typed_print_translation {*
@@ -325,9 +325,9 @@
   fun num_tr' show_sorts T [n] =
     let
       val k = int_of_num' n;
-      val t' = Syntax.const "_Numerals" $ Syntax.free ("#" ^ string_of_int k);
+      val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
     in case T
-     of Type ("fun", [_, T']) =>
+     of Type ("fun", [_, T']) =>  (* FIXME @{type_syntax} *)
          if not (! show_types) andalso can Term.dest_Type T' then t'
          else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
       | T' => if T' = dummyT then t' else raise Match
diff -r 724e8f77806a -r b271a8996f26 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOLCF/Cfun.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -40,8 +40,8 @@
 syntax "_cabs" :: "'a"
 
 parse_translation {*
-(* rewrites (_cabs x t) => (Abs_CFun (%x. t)) *)
-  [mk_binder_tr ("_cabs", @{const_syntax Abs_CFun})];
+(* rewrite (_cabs x t) => (Abs_CFun (%x. t)) *)
+  [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_CFun})];
 *}
 
 text {* To avoid eta-contraction of body: *}
@@ -49,13 +49,13 @@
   let
     fun cabs_tr' _ _ [Abs abs] = let
           val (x,t) = atomic_abs_tr' abs
-        in Syntax.const "_cabs" $ x $ t end
+        in Syntax.const @{syntax_const "_cabs"} $ x $ t end
 
       | cabs_tr' _ T [t] = let
           val xT = domain_type (domain_type T);
           val abs' = ("x",xT,(incr_boundvars 1 t)$Bound 0);
           val (x,t') = atomic_abs_tr' abs';
-        in Syntax.const "_cabs" $ x $ t' end;
+        in Syntax.const @{syntax_const "_cabs"} $ x $ t' end;
 
   in [(@{const_syntax Abs_CFun}, cabs_tr')] end;
 *}
@@ -69,26 +69,28 @@
   "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
 
 parse_ast_translation {*
-(* rewrites (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
-(* cf. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *)
+(* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
+(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
   let
     fun Lambda_ast_tr [pats, body] =
-          Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_cargs" pats, body)
+          Syntax.fold_ast_p @{syntax_const "_cabs"}
+            (Syntax.unfold_ast @{syntax_const "_cargs"} pats, body)
       | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
-  in [("_Lambda", Lambda_ast_tr)] end;
+  in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
 *}
 
 print_ast_translation {*
-(* rewrites (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *)
-(* cf. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *)
+(* rewrite (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *)
+(* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
   let
     fun cabs_ast_tr' asts =
-      (case Syntax.unfold_ast_p "_cabs"
-          (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of
+      (case Syntax.unfold_ast_p @{syntax_const "_cabs"}
+          (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of
         ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
       | (xs, body) => Syntax.Appl
-          [Syntax.Constant "_Lambda", Syntax.fold_ast "_cargs" xs, body]);
-  in [("_cabs", cabs_ast_tr')] end;
+          [Syntax.Constant @{syntax_const "_Lambda"},
+           Syntax.fold_ast @{syntax_const "_cargs"} xs, body]);
+  in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
 *}
 
 text {* Dummy patterns for continuous abstraction *}
diff -r 724e8f77806a -r b271a8996f26 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOLCF/Fixrec.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -226,10 +226,10 @@
   "_variable _noargs r" => "CONST unit_when\<cdot>r"
 
 parse_translation {*
-(* rewrites (_pat x) => (return) *)
-(* rewrites (_variable x t) => (Abs_CFun (%x. t)) *)
-  [("_pat", K (Syntax.const "Fixrec.return")),
-   mk_binder_tr ("_variable", "Abs_CFun")];
+(* rewrite (_pat x) => (return) *)
+(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *)
+ [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.return}),
+  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})];
 *}
 
 text {* Printing Case expressions *}
@@ -240,23 +240,26 @@
 print_translation {*
   let
     fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
-          (Syntax.const "_noargs", t)
+          (Syntax.const @{syntax_const "_noargs"}, t)
     |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
           let
             val (v1, t1) = dest_LAM t;
             val (v2, t2) = dest_LAM t1;
-          in (Syntax.const "_args" $ v1 $ v2, t2) end 
+          in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end
     |   dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
           let
-            val abs = case t of Abs abs => abs
+            val abs =
+              case t of Abs abs => abs
                 | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
             val (x, t') = atomic_abs_tr' abs;
-          in (Syntax.const "_variable" $ x, t') end
+          in (Syntax.const @{syntax_const "_variable"} $ x, t') end
     |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
 
     fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
-          let val (v, t) = dest_LAM r;
-          in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end;
+          let val (v, t) = dest_LAM r in
+            Syntax.const @{syntax_const "_Case1"} $
+              (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
+          end;
 
   in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
 *}
diff -r 724e8f77806a -r b271a8996f26 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOLCF/Sprod.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -51,7 +51,7 @@
   "ssplit = (\<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
 syntax
-  "@stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
+  "_stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
 translations
   "(:x, y, z:)" == "(:x, (:y, z:):)"
   "(:x, y:)"    == "CONST spair\<cdot>x\<cdot>y"
diff -r 724e8f77806a -r b271a8996f26 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Pure/Isar/proof_context.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -26,6 +26,7 @@
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val full_name: Proof.context -> binding -> string
+  val syn_of: Proof.context -> Syntax.syntax
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
   val the_const_constraint: Proof.context -> string -> typ
diff -r 724e8f77806a -r b271a8996f26 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -127,5 +127,10 @@
       let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
       in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
 
+val _ = inline "syntax_const"
+  (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
+    if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
+    else error ("Unknown syntax const: " ^ quote c)));
+
 end;
 
diff -r 724e8f77806a -r b271a8996f26 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Pure/Syntax/syn_ext.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -401,7 +401,7 @@
    Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
    Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
    Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
-  []
+  standard_token_markers
   ([], [], [], [])
   []
   ([], []);
diff -r 724e8f77806a -r b271a8996f26 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Pure/Syntax/syntax.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -54,6 +54,7 @@
     PrintRule of 'a * 'a |
     ParsePrintRule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
+  val is_const: syntax -> string -> bool
   val standard_unparse_term: (string -> xstring) ->
     Proof.context -> syntax -> bool -> term -> Pretty.T
   val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
@@ -592,6 +593,8 @@
   | print_rule (ParsePrintRule pats) = SOME (swap pats);
 
 
+fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
+
 local
 
 fun check_rule (rule as (lhs, rhs)) =
@@ -603,11 +606,9 @@
 
 fun read_pattern ctxt is_logtype syn (root, str) =
   let
-    val Syntax ({consts, ...}, _) = syn;
-
     fun constify (ast as Ast.Constant _) = ast
       | constify (ast as Ast.Variable x) =
-          if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x
+          if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
           else ast
       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
 
diff -r 724e8f77806a -r b271a8996f26 src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/ILL.thy	Thu Feb 11 23:50:38 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
 
diff -r 724e8f77806a -r b271a8996f26 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/LK0.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,10 +1,9 @@
 (*  Title:      LK/LK0.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 There may be printing problems if a seqent is in expanded normal form
-        (eta-expanded, beta-contracted)
+(eta-expanded, beta-contracted).
 *)
 
 header {* Classical First-Order Sequent Calculus *}
@@ -35,10 +34,10 @@
   Ex           :: "('a => o) => o"   (binder "EX " 10)
 
 syntax
- "@Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "_Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
 
-parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
-print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
+parse_translation {* [(@{syntax_const "_Trueprop"}, two_seq_tr @{const_syntax Trueprop})] *}
+print_translation {* [(@{const_syntax Trueprop}, two_seq_tr' @{syntax_const "_Trueprop"})] *}
 
 abbreviation
   not_equal  (infixl "~=" 50) where
diff -r 724e8f77806a -r b271a8996f26 src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/Modal0.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/Modal0.thy
-    ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
@@ -18,21 +17,23 @@
   Rstar         :: "two_seqi"
 
 syntax
-  "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
-  "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
+  "_Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
+  "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
 
 ML {*
-  val Lstar = "Lstar";
-  val Rstar = "Rstar";
-  val SLstar = "@Lstar";
-  val SRstar = "@Rstar";
-
-  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] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
+  fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
 *}
 
-parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
-print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
+parse_translation {*
+ [(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}),
+  (@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})]
+*}
+
+print_translation {*
+ [(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}),
+  (@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})]
+*}
 
 defs
   strimp_def:    "P --< Q == [](P --> Q)"
diff -r 724e8f77806a -r b271a8996f26 src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/S43.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Modal/S43.thy
-    ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 
@@ -14,25 +13,24 @@
   S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
              seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
 syntax
-  "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
+  "_S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
                          ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
 
-ML {*
-  val S43pi  = "S43pi";
-  val SS43pi = "@S43pi";
-
-  val tr  = seq_tr;
-  val tr' = seq_tr';
-
-  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
-        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
-  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
-        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
-
+parse_translation {*
+  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"}, s43pi_tr)] end
 *}
 
-parse_translation {* [(SS43pi,s43pi_tr)] *}
-print_translation {* [(S43pi,s43pi_tr')] *}
+print_translation {*
+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}, s43pi_tr')] end
+*}
 
 axioms
 (* Definition of the star operation using a set of Horn clauses  *)
diff -r 724e8f77806a -r b271a8996f26 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/Sequents.thy	Thu Feb 11 23:50:38 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"
 
diff -r 724e8f77806a -r b271a8996f26 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/Bin.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -26,11 +26,6 @@
         | Min
         | Bit ("w: bin", "b: bool")     (infixl "BIT" 90)
 
-use "Tools/numeral_syntax.ML"
-
-syntax
-  "_Int"    :: "xnum => i"        ("_")
-
 consts
   integ_of  :: "i=>i"
   NCons     :: "[i,i]=>i"
@@ -106,6 +101,10 @@
     "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
                                  NCons(bin_mult(v,w),0))"
 
+syntax
+  "_Int"    :: "xnum => i"        ("_")
+
+use "Tools/numeral_syntax.ML"
 setup NumeralSyntax.setup
 
 
diff -r 724e8f77806a -r b271a8996f26 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/Induct/Multiset.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -74,9 +74,9 @@
   "a :# M == a \<in> mset_of(M)"
 
 syntax
-  "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
+  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
 syntax (xsymbols)
-  "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
+  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, %x. P)"
 
diff -r 724e8f77806a -r b271a8996f26 src/ZF/List_ZF.thy
--- a/src/ZF/List_ZF.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/List_ZF.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -16,7 +16,7 @@
 
 syntax
  "[]"        :: i                                       ("[]")
- "@List"     :: "is => i"                                 ("[(_)]")
+ "_List"     :: "is => i"                                 ("[(_)]")
 
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
diff -r 724e8f77806a -r b271a8996f26 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/OrdQuant.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -23,9 +23,9 @@
     "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
 
 syntax
-  "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
-  "@oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
-  "@OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
+  "_oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
+  "_oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
+  "_OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
 
 translations
   "ALL x<a. P"  == "CONST oall(a, %x. P)"
@@ -33,13 +33,13 @@
   "UN x<a. B"   == "CONST OUnion(a, %x. B)"
 
 syntax (xsymbols)
-  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
-  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
-  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
+  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
+  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
+  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
 syntax (HTML output)
-  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
-  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
-  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
+  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
+  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
+  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
 
 
 subsubsection {*simplification of the new quantifiers*}
@@ -203,15 +203,15 @@
     "rex(M, P) == EX x. M(x) & P(x)"
 
 syntax
-  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
-  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3EX _[_]./ _)" 10)
+  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
+  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3EX _[_]./ _)" 10)
 
 syntax (xsymbols)
-  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
-  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
+  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
+  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
 syntax (HTML output)
-  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
-  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
+  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
+  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
 
 translations
   "ALL x[M]. P"  == "CONST rall(M, %x. P)"
diff -r 724e8f77806a -r b271a8996f26 src/ZF/Tools/numeral_syntax.ML
--- a/src/ZF/Tools/numeral_syntax.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/Tools/numeral_syntax.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -7,92 +7,83 @@
 
 signature NUMERAL_SYNTAX =
 sig
-  val dest_bin : term -> int
-  val mk_bin   : int -> term
-  val int_tr   : term list -> term
-  val int_tr'  : bool -> typ -> term list -> term
-  val setup    : theory -> theory
+  val make_binary: int -> int list
+  val dest_binary: int list -> int
+  val int_tr: term list -> term
+  val int_tr': bool -> typ -> term list -> term
+  val setup: theory -> theory
 end;
 
 structure NumeralSyntax: NUMERAL_SYNTAX =
 struct
 
-(* Bits *)
+(* bits *)
 
-fun mk_bit 0 = @{term "0"}
-  | mk_bit 1 = @{term "succ(0)"}
+fun mk_bit 0 = Syntax.const @{const_syntax "0"}
+  | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
   | mk_bit _ = sys_error "mk_bit";
 
-fun dest_bit (Const (@{const_name "0"}, _)) = 0
-  | dest_bit (Const (@{const_name succ}, _) $ Const (@{const_name "0"}, _)) = 1
+fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
+  | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
   | dest_bit _ = raise Match;
 
 
-(* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
+(* bit strings *)
+
+fun make_binary 0 = []
+  | make_binary ~1 = [~1]
+  | make_binary n = (n mod 2) :: make_binary (n div 2);
 
+fun dest_binary [] = 0
+  | dest_binary (b :: bs) = b + 2 * dest_binary bs;
+
+
+(*try to handle superfluous leading digits nicely*)
 fun prefix_len _ [] = 0
   | prefix_len pred (x :: xs) =
       if pred x then 1 + prefix_len pred xs else 0;
 
 fun mk_bin i =
-  let fun bin_of_int 0  = []
-        | bin_of_int ~1 = [~1]
-        | bin_of_int n  = (n mod 2) :: bin_of_int (n div 2);
-
-      fun term_of [] = @{const Pls}
-            | term_of [~1] = @{const Min}
-            | term_of (b :: bs) = @{const Bit} $ term_of bs $ mk_bit b;
-  in
-    term_of (bin_of_int i)
-  end;
+  let
+    fun term_of [] = Syntax.const @{const_syntax Pls}
+      | term_of [~1] = Syntax.const @{const_syntax Min}
+      | term_of (b :: bs) = Syntax.const @{const_syntax Bit} $ term_of bs $ mk_bit b;
+  in term_of (make_binary i) end;
 
-(*we consider all "spellings", since they could vary depending on the caller*)
-fun bin_of (Const ("Pls", _)) = []
-  | bin_of (Const ("bin.Pls", _)) = []
-  | bin_of (Const ("Bin.bin.Pls", _)) = []
-  | bin_of (Const ("Min", _)) = [~1]
-  | bin_of (Const ("bin.Min", _)) = [~1]
-  | bin_of (Const ("Bin.bin.Min", _)) = [~1]
-  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
-  | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
-  | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+fun bin_of (Const (@{const_syntax Pls}, _)) = []
+  | bin_of (Const (@{const_syntax Min}, _)) = [~1]
+  | bin_of (Const (@{const_syntax Bit}, _) $ bs $ b) = dest_bit b :: bin_of bs
   | bin_of _ = raise Match;
 
-(*Convert a list of bits to an integer*)
-fun integ_of [] = 0
-  | integ_of (b :: bs) = b + 2 * integ_of bs;
-
-val dest_bin = integ_of o bin_of;
-
-(*leading 0s and (for negative numbers) -1s cause complications, though they 
+(*Leading 0s and (for negative numbers) -1s cause complications, though they 
   should never arise in normal use. The formalization used in HOL prevents 
   them altogether.*)
 fun show_int t =
   let
     val rev_digs = bin_of t;
     val (sign, zs) =
-        (case rev rev_digs of
-             ~1 :: bs => ("-", prefix_len (equal 1) bs)
-           | bs =>       ("",  prefix_len (equal 0) bs));
-    val num = string_of_int (abs (integ_of rev_digs));
+      (case rev rev_digs of
+         ~1 :: bs => ("-", prefix_len (equal 1) bs)
+      | bs => ("",  prefix_len (equal 0) bs));
+    val num = string_of_int (abs (dest_binary rev_digs));
   in
     "#" ^ sign ^ implode (replicate zs "0") ^ num
   end;
 
 
-
 (* translation of integer constant tokens to and from binary *)
 
 fun int_tr (*"_Int"*) [t as Free (str, _)] =
-      Syntax.const "integ_of" $ mk_bin (#value (Syntax.read_xnum str))
+      Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
   | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
 
-fun int_tr' _ _ (*"integ_of"*) [t] = Syntax.const "_Int" $ Syntax.free (show_int t)
-  | int_tr' (_:bool) (_:typ)     _ = raise Match;
+fun int_tr' _ _ (*"integ_of"*) [t] =
+      Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
+  | int_tr' (_: bool) (_: typ) _ = raise Match;
 
 
 val setup =
- (Sign.add_trfuns ([], [("_Int", int_tr)], [], []) #>
-  Sign.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
+ (Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [], []) #>
+  Sign.add_trfunsT [(@{const_syntax integ_of}, int_tr')]);
 
 end;
diff -r 724e8f77806a -r b271a8996f26 src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/UNITY/Union.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -41,8 +41,8 @@
       SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
   
 syntax
-  "@JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
-  "@JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
+  "_JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
+  "_JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
 
 translations
   "JN x:A. B"   == "CONST JOIN(A, (%x. B))"
@@ -54,8 +54,8 @@
   Join  (infixl "\<squnion>" 65)
 
 syntax (xsymbols)
-  "@JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
-  "@JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
+  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
+  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
 
 
 subsection{*SKIP*}
diff -r 724e8f77806a -r b271a8996f26 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/ZF.thy	Thu Feb 11 23:50:38 2010 +0100
@@ -105,26 +105,26 @@
 
 syntax
   ""          :: "i => is"                   ("_")
-  "@Enum"     :: "[i, is] => is"             ("_,/ _")
+  "_Enum"     :: "[i, is] => is"             ("_,/ _")
 
-  "@Finset"   :: "is => i"                   ("{(_)}")
-  "@Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
-  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
-  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
-  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
-  "@INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
-  "@UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
-  "@PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
-  "@SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
-  "@lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
-  "@Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
-  "@Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
+  "_Finset"   :: "is => i"                   ("{(_)}")
+  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
+  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
+  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
+  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
+  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
 
   (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
 
-  "@pattern"  :: "patterns => pttrn"         ("<_>")
+  "_pattern"  :: "patterns => pttrn"         ("<_>")
   ""          :: "pttrn => patterns"         ("_")
-  "@patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
+  "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
 
 translations
   "{x, xs}"     == "CONST cons(x, {xs})"
@@ -158,18 +158,18 @@
   Inter           ("\<Inter>_" [90] 90)
 
 syntax (xsymbols)
-  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
-  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
-  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
-  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
-  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
-  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
-  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
-  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
-  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
-  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
-  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
-  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
+  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
+  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
+  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
+  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
+  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
 
 notation (HTML output)
   cart_prod       (infixr "\<times>" 80) and
@@ -182,18 +182,18 @@
   Inter           ("\<Inter>_" [90] 90)
 
 syntax (HTML output)
-  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
-  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
-  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
-  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
-  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
-  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
-  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
-  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
-  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
-  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
-  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
-  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
+  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
+  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
+  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
+  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
+  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
 
 
 finalconsts
diff -r 724e8f77806a -r b271a8996f26 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/int_arith.ML	Thu Feb 11 23:50:38 2010 +0100
@@ -7,15 +7,40 @@
 structure Int_Numeral_Simprocs =
 struct
 
+(* abstract syntax operations *)
+
+fun mk_bit 0 = @{term "0"}
+  | mk_bit 1 = @{term "succ(0)"}
+  | mk_bit _ = sys_error "mk_bit";
+
+fun dest_bit @{term "0"} = 0
+  | dest_bit @{term "succ(0)"} = 1
+  | dest_bit _ = raise Match;
+
+fun mk_bin i =
+  let
+    fun term_of [] = @{term Pls}
+      | term_of [~1] = @{term Min}
+      | term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b;
+  in term_of (NumeralSyntax.make_binary i) end;
+
+fun dest_bin tm =
+  let
+    fun bin_of @{term Pls} = []
+      | bin_of @{term Min} = [~1]
+      | bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
+      | bin_of _ = sys_error "dest_bin";
+  in NumeralSyntax.dest_binary (bin_of tm) end;
+
+
 (*Utilities*)
 
-fun mk_numeral n = @{const integ_of} $ NumeralSyntax.mk_bin n;
+fun mk_numeral i = @{const integ_of} $ mk_bin i;
 
 (*Decodes a binary INTEGER*)
 fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
-     (NumeralSyntax.dest_bin w
-      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
-  | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+     (dest_bin w handle SYS_ERROR _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
 
 fun find_first_numeral past (t::terms) =
         ((dest_numeral t, rev past @ terms)