# HG changeset patch
# User wenzelm
# Date 1265923198 -3600
# Node ID 1a0c129bb2e003c0d14edabd4c2c923f69437b1a
# Parent  ff6f60e6ab8580da9961cca01c7d0e29323b4552
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};

diff -r ff6f60e6ab85 -r 1a0c129bb2e0 doc-src/Classes/Thy/Setup.thy
--- a/doc-src/Classes/Thy/Setup.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/doc-src/Classes/Thy/Setup.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/CCL/Set.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/CCL/Term.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/CCL/Type.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Cube/Cube.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/FOLP/IFOLP.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Hoare/HeapSyntax.thy
--- a/src/HOL/Hoare/HeapSyntax.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare/HeapSyntax.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Hoare/HeapSyntaxAbort.thy
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare/Separation.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Hoare_Parallel/OG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -46,14 +46,14 @@
 translations
   "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 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 True THEN c END"
+  "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END"
   "r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
  
 nonterminals
@@ -77,14 +77,14 @@
 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 (@{const_syntax Collect}, _) $ t) :: ts) =
           quote_tr' (Syntax.const name) (t :: ts)
@@ -100,7 +100,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;
@@ -112,24 +112,24 @@
       | 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 (@{const_syntax Cons}, _) $
             (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some},_) $ t1 ) $ t2) $
-            Const (@{const_syntax Nil}, _))] = Syntax.const "_prg" $ 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 "_prgs" $ t1 $ t2 $ Parallel_PAR [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
    [(@{const_syntax Collect}, assert_tr'),
     (@{const_syntax Basic}, assign_tr'),
diff -r ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Hoare_Parallel/Quote_Antiquote.thy
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -16,9 +16,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
 *}
 
 end
\ No newline at end of file
diff -r ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Hoare_Parallel/RG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -20,11 +20,11 @@
 
 translations
   "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
-  "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 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
@@ -59,10 +59,10 @@
 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 (@{const_syntax Collect}, _) $ t) :: ts) =
           quote_tr' (Syntax.const name) (t :: ts)
@@ -74,7 +74,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;
@@ -86,14 +86,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
    [(@{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 Cond}, bexp_tr' @{syntax_const "_Cond"}),
+    (@{const_syntax While}, bexp_tr' @{syntax_const "_While"})]
   end
 *}
 
diff -r ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/ex/Antiquote.thy
--- a/src/HOL/ex/Antiquote.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/ex/Antiquote.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/ex/Binary.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/ex/Multiquote.thy
--- a/src/HOL/ex/Multiquote.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/ex/Multiquote.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/ex/Numeral.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Sequents/ILL.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/ILL.thy
-    ID:         $Id$
     Author:     Sara Kalvala and Valeria de Paiva
     Copyright   1995  University of Cambridge
 *)
@@ -32,19 +31,21 @@
   PromAux :: "three_seqi"
 
 syntax
-  "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
-  "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
-  "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
+  "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
+  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
+  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
 
 parse_translation {*
-  [("@Trueprop", single_tr "Trueprop"),
-   ("@Context", two_seq_tr "Context"),
-   ("@PromAux", three_seq_tr "PromAux")] *}
+  [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
+   (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
+   (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
+*}
 
 print_translation {*
-  [("Trueprop", single_tr' "@Trueprop"),
-   ("Context", two_seq_tr'"@Context"),
-   ("PromAux", three_seq_tr'"@PromAux")] *}
+  [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
+   (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
+   (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
+*}
 
 defs
 
diff -r ff6f60e6ab85 -r 1a0c129bb2e0 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Sequents/LK0.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Sequents/Modal0.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Sequents/S43.thy	Thu Feb 11 22:19:58 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 ff6f60e6ab85 -r 1a0c129bb2e0 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Sequents/Sequents.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/Sequents.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
@@ -36,14 +35,14 @@
 
 
 syntax
- SeqEmp         :: seq                                  ("")
- SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
+ "_SeqEmp"         :: seq                                  ("")
+ "_SeqApp"         :: "[seqobj,seqcont] => seq"            ("__")
 
- SeqContEmp     :: seqcont                              ("")
- SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
+ "_SeqContEmp"     :: seqcont                              ("")
+ "_SeqContApp"     :: "[seqobj,seqcont] => seqcont"        (",/ __")
 
- SeqO           :: "o => seqobj"                        ("_")
- SeqId          :: "'a => seqobj"                       ("$_")
+ "_SeqO"           :: "o => seqobj"                        ("_")
+ "_SeqId"          :: "'a => seqobj"                       ("$_")
 
 types
  single_seqe = "[seq,seqobj] => prop"
@@ -60,86 +59,76 @@
 
 syntax
   (*Constant to allow definitions of SEQUENCES of formulas*)
-  "@Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
+  "_Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
 
 ML {*
 
 (* parse translation for sequences *)
 
-fun abs_seq' t = Abs("s", Type("seq'",[]), t);
+fun abs_seq' t = Abs ("s", Type ("seq'", []), t);   (* FIXME @{type_syntax} *)
 
-fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
-    seqobj_tr(_ $ i) = i;
-
-fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
-    seqcont_tr(Const("SeqContApp",_) $ so $ sc) =
-      (seqobj_tr so) $ (seqcont_tr sc);
+fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
+      Const (@{const_syntax SeqO'}, dummyT) $ f
+  | seqobj_tr (_ $ i) = i;
 
-fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
-    seq_tr(Const("SeqApp",_) $ so $ sc) =
-      abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
+fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0
+  | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) =
+      seqobj_tr so $ seqcont_tr sc;
 
+fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0)
+  | seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) =
+      abs_seq'(seqobj_tr so $ seqcont_tr sc);
 
-fun singlobj_tr(Const("SeqO",_) $ f) =
-    abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
-
+fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) =
+  abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0);
 
 
 (* print translation for sequences *)
 
 fun seqcont_tr' (Bound 0) =
-      Const("SeqContEmp",dummyT) |
-    seqcont_tr' (Const("SeqO'",_) $ f $ s) =
-      Const("SeqContApp",dummyT) $
-      (Const("SeqO",dummyT) $ f) $
-      (seqcont_tr' s) |
-(*    seqcont_tr' ((a as Abs(_,_,_)) $ s)=
-      seqcont_tr'(Term.betapply(a,s)) | *)
-    seqcont_tr' (i $ s) =
-      Const("SeqContApp",dummyT) $
-      (Const("SeqId",dummyT) $ i) $
-      (seqcont_tr' s);
+      Const (@{syntax_const "_SeqContEmp"}, dummyT)
+  | seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
+      Const (@{syntax_const "_SeqContApp"}, dummyT) $
+        (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
+  | seqcont_tr' (i $ s) =
+      Const (@{syntax_const "_SeqContApp"}, dummyT) $
+        (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s;
 
 fun seq_tr' s =
-    let fun seq_itr' (Bound 0) =
-              Const("SeqEmp",dummyT) |
-            seq_itr' (Const("SeqO'",_) $ f $ s) =
-              Const("SeqApp",dummyT) $
-              (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
-(*            seq_itr' ((a as Abs(_,_,_)) $ s) =
-              seq_itr'(Term.betapply(a,s)) |    *)
-            seq_itr' (i $ s) =
-              Const("SeqApp",dummyT) $
-              (Const("SeqId",dummyT) $ i) $
-              (seqcont_tr' s)
-    in case s of
-         Abs(_,_,t) => seq_itr' t |
-         _ => s $ (Bound 0)
-    end;
+  let
+    fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT)
+      | seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
+          Const (@{syntax_const "_SeqApp"}, dummyT) $
+            (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
+      | seq_itr' (i $ s) =
+          Const (@{syntax_const "_SeqApp"}, dummyT) $
+            (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s
+  in
+    case s of
+      Abs (_, _, t) => seq_itr' t
+    | _ => s $ Bound 0
+  end;
 
 
+fun single_tr c [s1, s2] =
+  Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
+
+fun two_seq_tr c [s1, s2] =
+  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
+
+fun three_seq_tr c [s1, s2, s3] =
+  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
+
+fun four_seq_tr c [s1, s2, s3, s4] =
+  Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
 
 
-fun single_tr c [s1,s2] =
-    Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
-
-fun two_seq_tr c [s1,s2] =
-    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
-
-fun three_seq_tr c [s1,s2,s3] =
-    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
-
-fun four_seq_tr c [s1,s2,s3,s4] =
-    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
-
-
-fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
-    singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
+fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm
+  | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id;
 
 
 fun single_tr' c [s1, s2] =
-(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 );
-
+  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
 
 fun two_seq_tr' c [s1, s2] =
   Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
@@ -157,7 +146,7 @@
 fun side_tr [s1] = seq_tr s1;
 *}
 
-parse_translation {* [("@Side", side_tr)] *}
+parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
 
 use "prover.ML"