src/HOL/Tools/Old_Datatype/old_datatype_aux.ML

     case_rewrites : thm list,
     case_cong : thm,
     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 =
 sig
   include OLD_DATATYPE_COMMON

    case_cong : thm,
    case_cong_weak : thm,
    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)
   | subst_DtTFree i substs (DtType (name, ts)) = DtType (name, map (subst_DtTFree i substs) ts)
   | subst_DtTFree i _ (DtRec j) = DtRec (i + j);