--- a/Nominal/nominal_atoms.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_atoms.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -28,14 +28,13 @@
 
 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
   let
-    val _ = Theory.requires thy (Context.theory_name @{theory}) "nominal logic";
     val str = Sign.full_name thy name;
 
     (* typedef *)
     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 (name, [], NoSyn) set NONE tac thy;
+    fun 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 (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
     val newT = #abs_type (fst info);
@@ -77,7 +76,7 @@
 
 (** outer syntax **)
 val _ =
-  Outer_Syntax.command @{command_spec "atom_decl"}
+  Outer_Syntax.command @{command_keyword atom_decl}
     "declaration of a concrete atom type" 
       ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
         (Toplevel.theory o add_atom_decl))