src/HOL/Nominal/Nominal.thy

 keywords
   "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
   "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
   "avoids"
 begin
+
+declare [[typedef_overloaded]]
+
 
 section {* Permutations *}
 (*======================*)
 
 type_synonym 

   where
   ABS_in: "(abs_fun a x)\<in>ABS_set"
 
 definition "ABS = ABS_set"
 
-typedef ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+typedef ('x, 'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
     "ABS::('x\<Rightarrow>('a noption)) set"
   morphisms Rep_ABS Abs_ABS
   unfolding ABS_def
 proof 
   fix x::"'a" and a::"'x"