Type abbreviations are permitted within a local theory target, but cannot refer to locally fixed type variables. So type_synonym is only half-localized (like typedecl and typedef).

This should be reconsidered eventually, but it will require to revisit many fine points in local theory targets, potentially also specification packages for types.

Example (e.g. Isabelle2019):

theory Scratch
  imports Main
begin

locale test = fixes x :: 'a
begin

type_synonym t = "'a × 'a" 
(*ERROR:
  Extra variables on rhs: "'a"
  The error(s) above occurred in type abbreviation "t"
*)

end

end