# HG changeset patch
# User wenzelm
# Date 1265660907 -3600
# Node ID a5db9779b0263d5204a9a813351e56a1644f1373
# Parent  43175817d83b58f88d0bccf6720feda027a9f3c2
modernized some syntax translations;

diff -r 43175817d83b -r a5db9779b026 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/CCL/Set.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -40,11 +40,11 @@
   "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
 
 translations
-  "{x. P}"      == "Collect(%x. P)"
-  "INT x:A. B"  == "INTER(A, %x. B)"
-  "UN x:A. B"   == "UNION(A, %x. B)"
-  "ALL x:A. P"  == "Ball(A, %x. P)"
-  "EX x:A. P"   == "Bex(A, %x. P)"
+  "{x. P}"      == "CONST Collect(%x. P)"
+  "INT x:A. B"  == "CONST INTER(A, %x. B)"
+  "UN x:A. B"   == "CONST UNION(A, %x. B)"
+  "ALL x:A. P"  == "CONST Ball(A, %x. P)"
+  "EX x:A. P"   == "CONST Bex(A, %x. P)"
 
 local
 
diff -r 43175817d83b -r a5db9779b026 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/CCL/Type.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -39,15 +39,15 @@
   "@Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
 
 translations
-  "PROD x:A. B" => "Pi(A, %x. B)"
-  "A -> B"      => "Pi(A, %_. B)"
-  "SUM x:A. B"  => "Sigma(A, %x. B)"
-  "A * B"       => "Sigma(A, %_. B)"
-  "{x: A. B}"   == "Subtype(A, %x. B)"
+  "PROD x:A. B" => "CONST Pi(A, %x. B)"
+  "A -> B"      => "CONST Pi(A, %_. B)"
+  "SUM x:A. B"  => "CONST Sigma(A, %x. B)"
+  "A * B"       => "CONST Sigma(A, %_. B)"
+  "{x: A. B}"   == "CONST Subtype(A, %x. B)"
 
 print_translation {*
-  [("Pi", dependent_tr' ("@Pi", "@->")),
-   ("Sigma", dependent_tr' ("@Sigma", "@*"))] *}
+  [(@{const_syntax Pi}, dependent_tr' ("@Pi", "@->")),
+   (@{const_syntax Sigma}, dependent_tr' ("@Sigma", "@*"))] *}
 
 axioms
   Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
diff -r 43175817d83b -r a5db9779b026 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/CTT/CTT.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -63,8 +63,8 @@
   "_PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
   "_SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
 translations
-  "PROD x:A. B" == "Prod(A, %x. B)"
-  "SUM x:A. B"  == "Sum(A, %x. B)"
+  "PROD x:A. B" == "CONST Prod(A, %x. B)"
+  "SUM x:A. B"  == "CONST Sum(A, %x. B)"
 
 abbreviation
   Arrow     :: "[t,t]=>t"  (infixr "-->" 30) where
diff -r 43175817d83b -r a5db9779b026 src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/Cube/Cube.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -43,9 +43,9 @@
 
 translations
   ("prop") "x:X" == ("prop") "|- x:X"
-  "Lam x:A. B"   == "Abs(A, %x. B)"
-  "Pi x:A. B"    => "Prod(A, %x. B)"
-  "A -> B"       => "Prod(A, %_. B)"
+  "Lam x:A. B"   == "CONST Abs(A, %x. B)"
+  "Pi x:A. B"    => "CONST Prod(A, %x. B)"
+  "A -> B"       => "CONST Prod(A, %_. B)"
 
 syntax (xsymbols)
   Trueprop      :: "[context', typing'] => prop"        ("(_/ \<turnstile> _)")
@@ -54,7 +54,7 @@
   Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
   arrow         :: "[term, term] => term"               (infixr "\<rightarrow>" 10)
 
-print_translation {* [("Prod", dependent_tr' ("Pi", "arrow"))] *}
+print_translation {* [(@{const_syntax Prod}, dependent_tr' ("Pi", "arrow"))] *}
 
 axioms
   s_b:          "*: []"
diff -r 43175817d83b -r a5db9779b026 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/FOL/IFOL.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -772,7 +772,7 @@
 
 translations
   "_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)"
 
 
 lemma LetI: 
diff -r 43175817d83b -r a5db9779b026 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -302,7 +302,7 @@
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
       ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
-  "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"
+  "\<Otimes>\<index>i:A. b" == "CONST finprod \<struct>\<index> (%i. b) A"
   -- {* Beware of argument permutation! *}
 
 lemma (in comm_monoid) finprod_empty [simp]: 
diff -r 43175817d83b -r a5db9779b026 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Algebra/Ring.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -213,7 +213,7 @@
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
       ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
-  "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"
+  "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A"
   -- {* Beware of argument permutation! *}
 
 context abelian_monoid begin
diff -r 43175817d83b -r a5db9779b026 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Auth/Message.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -58,7 +58,7 @@
 
 translations
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
-  "{|x, y|}"      == "MPair x y"
+  "{|x, y|}"      == "CONST MPair x y"
 
 
 constdefs
diff -r 43175817d83b -r a5db9779b026 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -15,11 +15,8 @@
 datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
   | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
 
-ML{* @{term "Add"}*}
-syntax "_poly0" :: "poly" ("0\<^sub>p")
-translations "0\<^sub>p" \<rightleftharpoons> "C (0\<^sub>N)"
-syntax "_poly" :: "int \<Rightarrow> poly" ("_\<^sub>p")
-translations "i\<^sub>p" \<rightleftharpoons> "C (i\<^sub>N)"
+abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
+abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
 
 subsection{* Boundedness, substitution and all that *}
 consts polysize:: "poly \<Rightarrow> nat"
@@ -117,14 +114,14 @@
   polysub :: "poly\<times>poly \<Rightarrow> poly"
   polymul :: "poly\<times>poly \<Rightarrow> poly"
   polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
-syntax "_polyadd" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
-translations "a +\<^sub>p b" \<rightleftharpoons> "polyadd (a,b)"  
-syntax "_polymul" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
-translations "a *\<^sub>p b" \<rightleftharpoons> "polymul (a,b)"  
-syntax "_polysub" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
-translations "a -\<^sub>p b" \<rightleftharpoons> "polysub (a,b)"  
-syntax "_polypow" :: "nat \<Rightarrow> poly \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
-translations "a ^\<^sub>p k" \<rightleftharpoons> "polypow k a" 
+abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
+  where "a +\<^sub>p b \<equiv> polyadd (a,b)"
+abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
+  where "a *\<^sub>p b \<equiv> polymul (a,b)"
+abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
+  where "a -\<^sub>p b \<equiv> polysub (a,b)"
+abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
+  where "a ^\<^sub>p k \<equiv> polypow k a"
 
 recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
   "polyadd (C c, C c') = C (c+\<^sub>Nc')"
@@ -243,8 +240,9 @@
   "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
   "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
   "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
-syntax "_Ipoly" :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
-translations "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup>" \<rightleftharpoons> "Ipoly bs p"  
+abbreviation
+  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
+  where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
 
 lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" 
   by (simp add: INum_def)
diff -r 43175817d83b -r a5db9779b026 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -24,12 +24,7 @@
    | 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)
   
-syntax
-  "@assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
-  "@annskip" :: "'a com"                    ("SKIP")
-
-translations
-            "SKIP" == "Basic id"
+abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 types 'a sem = "'a => 'a => bool"
 
@@ -50,16 +45,19 @@
   "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
 
 
-syntax
- "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
-                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax ("" output)
- "@hoare"      :: "['a assn,'a com,'a assn] => bool"
-                 ("{_} // _ // {_}" [0,55,0] 50)
 
 (** parse translations **)
 
-ML{*
+syntax
+  "_assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
+
+syntax
+ "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
+                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
+syntax ("" output)
+ "_hoare"      :: "['a assn,'a com,'a assn] => bool"
+                 ("{_} // _ // {_}" [0,55,0] 50)
+ML {*
 
 local
 
@@ -91,7 +89,7 @@
 *}
 (* com_tr *)
 ML{*
-fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
+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 =
@@ -123,7 +121,7 @@
 end
 *}
 
-parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
+parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
 
 
 (*****************************************************************************)
@@ -175,8 +173,8 @@
 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 "@skip" end;
+  in if ch then 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
@@ -190,10 +188,10 @@
 
 
 fun spec_tr' [p, c, q] =
-  Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
+  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
 *}
 
-print_translation {* [("Valid", spec_tr')] *}
+print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
diff -r 43175817d83b -r a5db9779b026 src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -21,12 +21,7 @@
    | 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)
   
-syntax
-  "@assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
-  "@annskip" :: "'a com"                    ("SKIP")
-
-translations
-            "SKIP" == "Basic id"
+abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 types 'a sem = "'a option => 'a option => bool"
 
@@ -51,16 +46,19 @@
   "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
 
 
-syntax
- "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
-                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax ("" output)
- "@hoare"      :: "['a assn,'a com,'a assn] => bool"
-                 ("{_} // _ // {_}" [0,55,0] 50)
 
 (** parse translations **)
 
-ML{*
+syntax
+  "_assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
+
+syntax
+  "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
+                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
+syntax ("" output)
+  "_hoare"      :: "['a assn,'a com,'a assn] => bool"
+                 ("{_} // _ // {_}" [0,55,0] 50)
+ML {*
 
 local
 fun free a = Free(a,dummyT)
@@ -92,7 +90,7 @@
 *}
 (* com_tr *)
 ML{*
-fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
+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 =
@@ -124,7 +122,7 @@
 end
 *}
 
-parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
+parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
 
 
 (*****************************************************************************)
@@ -176,8 +174,8 @@
 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 "@skip" end;
+  in if ch then 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
@@ -191,10 +189,10 @@
 
 
 fun spec_tr' [p, c, q] =
-  Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
+  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
 *}
 
-print_translation {* [("Valid", spec_tr')] *}
+print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
 
 (*** The proof rules ***)
 
@@ -257,7 +255,7 @@
 
 syntax
   guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
-  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70,65] 61)
+  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
 translations
   "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
   "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
diff -r 43175817d83b -r a5db9779b026 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -228,11 +228,11 @@
   "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
 
 translations
-  ".{b}."                   => "Collect .(b)."
+  ".{b}."                   => "CONST Collect .(b)."
   "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
-  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
-  "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
-  "WHILE b INV i DO c OD"   => "While .{b}. i c"
+  "\<acute>x := a"                 => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
+  "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"
+  "WHILE b INV i DO c OD"   => "CONST While .{b}. i c"
   "WHILE b DO c OD"         == "WHILE b INV CONST undefined DO c OD"
 
 parse_translation {*
diff -r 43175817d83b -r a5db9779b026 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -52,7 +52,7 @@
 
 translations
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
-  "{|x, y|}"      == "MPair x y"
+  "{|x, y|}"      == "CONST MPair x y"
 
 
 constdefs
diff -r 43175817d83b -r a5db9779b026 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -78,11 +78,9 @@
           {S. S \<subseteq> pset cl &
            (| pset = S, order = induced S (order cl) |): CompleteLattice }"
 
-syntax
-  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
-
-translations
-  "S <<= cl" == "S : sublattice `` {cl}"
+abbreviation
+  sublattice_syntax :: "['a set, 'a potype] => bool" ("_ <<= _" [51, 50] 50)
+  where "S <<= cl \<equiv> S : sublattice `` {cl}"
 
 constdefs
   dual :: "'a potype => 'a potype"
diff -r 43175817d83b -r a5db9779b026 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -76,7 +76,7 @@
       ("(3PROD _:#_. _)" [0, 51, 10] 10)
 
 translations
-  "PROD i :# A. b" == "msetprod (%i. b) A"
+  "PROD i :# A. b" == "CONST msetprod (%i. b) A"
 
 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
   apply (simp add: msetprod_def power_add)
diff -r 43175817d83b -r a5db9779b026 src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -11,17 +11,14 @@
 theory PPROD imports Lift_prog begin
 
 constdefs
-
   PLam  :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
             => ((nat=>'b) * 'c) program"
     "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
 
 syntax
-  "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
-              ("(3plam _:_./ _)" 10)
-
+  "_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"  ("(3plam _:_./ _)" 10)
 translations
-  "plam x : A. B"   == "PLam A (%x. B)"
+  "plam x : A. B" == "CONST PLam A (%x. B)"
 
 
 (*** Basic properties ***)
diff -r 43175817d83b -r a5db9779b026 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/UNITY/Union.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -36,19 +36,19 @@
     "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
 
 syntax
-  "@JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
-  "@JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
+  "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
+  "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
 
 translations
-  "JN x : A. B"   == "JOIN A (%x. B)"
-  "JN x y. B"   == "JN x. JN y. B"
-  "JN x. B"     == "JOIN CONST UNIV (%x. B)"
+  "JN x: A. B" == "CONST JOIN A (%x. B)"
+  "JN x y. B" == "JN x. JN y. B"
+  "JN x. B" == "JOIN CONST UNIV (%x. B)"
 
 syntax (xsymbols)
   SKIP     :: "'a program"                              ("\<bottom>")
   Join     :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
-  "@JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
-  "@JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
+  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
+  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
 
 
 subsection{*SKIP*}
diff -r 43175817d83b -r a5db9779b026 src/Sequents/ILL_predlog.thy
--- a/src/Sequents/ILL_predlog.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/Sequents/ILL_predlog.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -22,8 +22,8 @@
 
   "[* A & B *]" == "[*A*] && [*B*]"
   "[* A | B *]" == "![*A*] ++ ![*B*]"
-  "[* - A *]"   == "[*A > ff*]"
-  "[* ff *]"    == "0"
+  "[* - A *]"   == "[*A > CONST ff*]"
+  "[* XCONST ff *]" == "0"
   "[* A = B *]" => "[* (A > B) & (B > A) *]"
 
   "[* A > B *]" == "![*A*] -o [*B*]"