--- a/Nominal/nominal_atoms.ML	Thu Oct 04 12:44:43 2012 +0100
+++ b/Nominal/nominal_atoms.ML	Fri Oct 19 09:40:24 2012 +0100
@@ -35,7 +35,7 @@
     val set = atom_decl_set str;
     val tac = rtac @{thm exists_eq_simple_sort} 1;
     val ((full_tname, info  as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
-      Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
+      Typedef.add_typedef_global (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
     val newT = #abs_type (fst info);