tuned signature;

--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 14 12:18:19 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 14 15:30:17 2011 +0100
@@ -6,7 +6,8 @@
 
 signature NOMINAL_DATATYPE =
 sig
-  val add_nominal_datatype : Datatype.config -> Datatype.spec_cmd list -> theory -> theory
+  val nominal_datatype : Datatype.config -> Datatype.spec list -> theory -> theory
+  val nominal_datatype_cmd : Datatype.config -> Datatype.spec_cmd list -> theory -> theory
   type descr
   type nominal_datatype_info
   val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
@@ -185,7 +186,7 @@
 fun fresh_star_const T U =
   Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
 
-fun gen_add_nominal_datatype prep_specs config dts thy =
+fun gen_nominal_datatype prep_specs config dts thy =
   let
     val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts;
 
@@ -2065,11 +2066,12 @@
     thy13
   end;
 
-val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_specs;
+val nominal_datatype = gen_nominal_datatype Datatype.check_specs;
+val nominal_datatype_cmd = gen_nominal_datatype Datatype.read_specs;
 
 val _ =
-  Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl
-    (Parse.and_list1 Datatype.spec_cmd
-      >> (Toplevel.theory o add_nominal_datatype Datatype.default_config));
+  Outer_Syntax.command "nominal_datatype" "define nominal datatypes" Keyword.thy_decl
+    (Parse.and_list1 Datatype.spec_cmd >>
+      (Toplevel.theory o nominal_datatype_cmd Datatype.default_config));
 
 end

--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Dec 14 12:18:19 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Dec 14 15:30:17 2011 +0100
@@ -19,7 +19,7 @@
   val read_specs: spec_cmd list -> theory -> spec list * Proof.context
   val check_specs: spec list -> theory -> spec list * Proof.context
   val add_datatype: config -> spec list -> theory -> string list * theory
-  val add_datatype_cmd: spec_cmd list -> theory -> theory
+  val add_datatype_cmd: config -> spec_cmd list -> theory -> string list * theory
   val spec_cmd: spec_cmd parser
 end;
 
@@ -798,7 +798,7 @@
   end;
 
 val add_datatype = gen_add_datatype check_specs;
-val add_datatype_cmd = snd oo gen_add_datatype read_specs Datatype_Aux.default_config;
+val add_datatype_cmd = gen_add_datatype read_specs;
 
 
 (* outer syntax *)
@@ -810,7 +810,8 @@
 
 val _ =
   Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
-    (Parse.and_list1 spec_cmd >> (Toplevel.theory o add_datatype_cmd));
+    (Parse.and_list1 spec_cmd
+      >> (Toplevel.theory o (snd oo add_datatype_cmd Datatype_Aux.default_config)));
 
 
 open Datatype_Data;