src/HOL/Product_Type.thy

 proof
   fix a b show "Pair_Rep a b : ?Prod"
     by blast
 qed
 
-syntax (symbols)
+syntax (xsymbols)
   "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
 syntax (HTML output)
   "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
 
 local

      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
 
   "SIGMA x:A. B" => "Sigma A (%x. B)"
   "A <*> B"      => "Sigma A (_K B)"
 
-syntax (symbols)
+syntax (xsymbols)
   "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
 
 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}