src/HOL/Tools/numeral_syntax.ML

   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) =  (* FIXME @{type_syntax} *)
+fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_syntax fun}, [_, T])) (t :: ts) =
       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
       in list_comb (t', ts) end
   | numeral_tr' _ (*"number_of"*) T (t :: ts) =