src/HOL/ex/Numeral.thy

           val {leading_zeros, value, ...} = Syntax.read_xnum num;
           val _ = leading_zeros = 0 andalso value > 0
             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 {*
 let
   fun dig b n = b + 2 * n; 

         dig 1 (int_of_num' n)
     | int_of_num' (Const (@{const_syntax One}, _)) = 1;
   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
     end;
 in [(@{const_syntax of_num}, num_tr')] end