# HG changeset patch
# User wenzelm
# Date 1265925622 -3600
# Node ID 446c5063e4fdcdd9b2abb56326c447844e4fd920
# Parent  b1fd1d756e208da4d9042998a096bb7f8cc3d0e6
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;

diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Fun.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/HOL.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Inductive.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Library/State_Monad.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/List.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Map.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Orderings.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Product_Type.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Set.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/SetInterval.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/String.thy
--- a/src/HOL/String.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/String.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Tools/float_syntax.ML
--- a/src/HOL/Tools/float_syntax.ML	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Tools/float_syntax.ML	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Typerep.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOLCF/Fixrec.thy	Thu Feb 11 23:00:22 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 b1fd1d756e20 -r 446c5063e4fd src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOLCF/Sprod.thy	Thu Feb 11 23:00:22 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"