more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;

--- a/src/HOL/Num.thy	Fri Mar 07 11:41:25 2014 +0100
+++ b/src/HOL/Num.thy	Fri Mar 07 11:46:26 2014 +0100
@@ -285,14 +285,14 @@
     fun num_of_int n =
       if n > 0 then
         (case IntInf.quotRem (n, 2) of
-          (0, 1) => Syntax.const @{const_name One}
-        | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
-        | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
+          (0, 1) => Syntax.const @{const_syntax One}
+        | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n
+        | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n)
       else raise Match
-    val numeral = Syntax.const @{const_name numeral}
-    val uminus = Syntax.const @{const_name uminus}
-    val one = Syntax.const @{const_name Groups.one}
-    val zero = Syntax.const @{const_name Groups.zero}
+    val numeral = Syntax.const @{const_syntax numeral}
+    val uminus = Syntax.const @{const_syntax uminus}
+    val one = Syntax.const @{const_syntax Groups.one}
+    val zero = Syntax.const @{const_syntax Groups.zero}
     fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
           c $ numeral_tr [t] $ u
       | numeral_tr [Const (num, _)] =
@@ -303,10 +303,10 @@
             if value > 0
             then numeral $ num_of_int value
             else if value = ~1 then uminus $ one
-            else uminus $ (numeral $ num_of_int (~value))
+            else uminus $ (numeral $ num_of_int (~ value))
           end
       | numeral_tr ts = raise TERM ("numeral_tr", ts);
-  in [("_Numeral", K numeral_tr)] end
+  in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
 *}
 
 typed_print_translation {*

--- a/src/HOL/Rat.thy	Fri Mar 07 11:41:25 2014 +0100
+++ b/src/HOL/Rat.thy	Fri Mar 07 11:46:26 2014 +0100
@@ -1155,12 +1155,16 @@
       let
         fun mk 1 = Syntax.const @{const_syntax Num.One}
           | mk i =
-              let val (q, r) = Integer.div_mod i 2
-              in HOLogic.mk_bit r $ (mk q) end;
+              let
+                val (q, r) = Integer.div_mod i 2;
+                val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1};
+              in Syntax.const bit $ (mk q) end;
       in
         if i = 0 then Syntax.const @{const_syntax Groups.zero}
         else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
-        else Syntax.const @{const_syntax Groups.uminus} $ (Syntax.const @{const_syntax Num.numeral} $ mk (~i))
+        else
+          Syntax.const @{const_syntax Groups.uminus} $
+            (Syntax.const @{const_syntax Num.numeral} $ mk (~ i))
       end;
 
     fun mk_frac str =
@@ -1181,6 +1185,7 @@
 lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
   by simp
 
+
 subsection {* Hiding implementation details *}
 
 hide_const (open) normalize positive

--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 11:41:25 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 11:46:26 2014 +0100
@@ -169,7 +169,7 @@
         fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
           | dest_case2 t = [t];
 
-        val errt = if err then @{term True} else @{term False};
+        val errt = Syntax.const (if err then @{const_syntax True} else @{const_syntax False});
       in
         Syntax.const @{const_syntax case_guard} $ errt $ t $
           (fold_rev