tuned signatures

--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -9,17 +9,15 @@
 
 signature OLD_DATATYPE =
 sig
+  include OLD_DATATYPE_COMMON
+
   val distinct_lemma: thm
-  type spec =
-    (binding * (string * sort) list * mixfix) *
-    (binding * typ list * mixfix) list
   type spec_cmd =
-    (binding * (string * string option) list * mixfix) *
-    (binding * string list * mixfix) list
+    (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list
   val read_specs: spec_cmd list -> theory -> spec list * Proof.context
   val check_specs: spec list -> theory -> spec list * Proof.context
-  val add_datatype: Old_Datatype_Aux.config -> spec list -> theory -> string list * theory
-  val add_datatype_cmd: Old_Datatype_Aux.config -> spec_cmd list -> theory -> string list * theory
+  val add_datatype: config -> spec list -> theory -> string list * theory
+  val add_datatype_cmd: config -> spec_cmd list -> theory -> string list * theory
   val spec_cmd: spec_cmd parser
 end;
 
@@ -663,8 +661,6 @@
 
 (* specifications *)
 
-type spec = (binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list;
-
 type spec_cmd =
   (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list;
 
@@ -674,7 +670,7 @@
   ((b, map (apsnd (Typedecl.read_constraint ctxt)) args, mx),
     constrs |> map (fn (c, Ts, mx') => (c, map (Syntax.parse_typ ctxt) Ts, mx')));
 
-fun check_specs ctxt (specs: spec list) =
+fun check_specs ctxt (specs: Old_Datatype_Aux.spec list) =
   let
     fun prep_spec ((tname, args, mx), constrs) tys =
       let
@@ -799,4 +795,6 @@
     (Parse.and_list1 spec_cmd
       >> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));
 
+open Old_Datatype_Aux;
+
 end;

--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -30,6 +30,7 @@
     case_cong_weak : thm,
     split : thm,
     split_asm: thm}
+  type spec = (binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list
 end
 
 signature OLD_DATATYPE_AUX =
@@ -199,6 +200,8 @@
    split : thm,
    split_asm: thm};
 
+type spec = (binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list;
+
 fun mk_Free s T i = Free (s ^ string_of_int i, T);
 
 fun subst_DtTFree _ substs (T as DtTFree a) = the_default T (AList.lookup (op =) substs a)