src/HOL/Typerep.thy

   in [(\<^syntax_const>\<open>_TYPEREP\<close>, K typerep_tr)] end
 \<close>
 
 typed_print_translation \<open>
   let
-    fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<open>\<^Type>\<open>itself T\<close>\<close> _\<close>
+    fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<^Type>\<open>itself T\<close> _\<close>
             (Const (\<^const_syntax>\<open>Pure.type\<close>, _) :: ts) =
           Term.list_comb
             (Syntax.const \<^syntax_const>\<open>_TYPEREP\<close> $ Syntax_Phases.term_of_typ ctxt T, ts)
       | typerep_tr' _ T ts = raise Match;
   in [(\<^const_syntax>\<open>typerep\<close>, typerep_tr')] end