diff -r 6ce0c8d59f5a -r ec121999a9cb src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Sun Oct 06 22:56:07 2024 +0200 +++ b/src/HOL/Typerep.thy Tue Oct 08 12:10:35 2024 +0200 @@ -18,7 +18,7 @@ end syntax - "_TYPEREP" :: "type => logic" (\(\indent=1 notation=\prefix TYPEREP\\TYPEREP/(1'(_')))\) + "_TYPEREP" :: "type => logic" (\(\indent=1 notation=\mixfix TYPEREP\\TYPEREP/(1'(_')))\) syntax_consts "_TYPEREP" \ typerep