diff -r 7bc38b93a1fc -r 9ae285ce814e Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/nominal_atoms.ML	Fri May 16 08:38:23 2014 +0100
@@ -28,7 +28,7 @@
 
 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
   let
-    val _ = Theory.requires thy "Nominal2_Base" "nominal logic";
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "nominal logic";
     val str = Sign.full_name thy name;
 
     (* typedef *)
@@ -80,6 +80,6 @@
   Outer_Syntax.command @{command_spec "atom_decl"}
     "declaration of a concrete atom type" 
       ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
-        (Toplevel.print oo (Toplevel.theory o add_atom_decl)))
+        (Toplevel.theory o add_atom_decl))
 
 end;