--- a/Nominal/nominal_atoms.ML	Tue Mar 16 17:20:46 2010 +0100
+++ b/Nominal/nominal_atoms.ML	Tue Mar 16 18:02:08 2010 +0100
@@ -44,7 +44,7 @@
     val set = atom_decl_set str;
     val tac = rtac @{thm exists_eq_simple_sort} 1;
     val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =
-      Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy;
+      Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
     val newT = #abs_type info;