src/HOL/Tools/Datatype/datatype_data.ML

 *)
 
 signature DATATYPE_DATA =
 sig
   include DATATYPE_COMMON
-  val derive_datatype_props : config -> string list -> string list option
-    -> descr list -> (string * sort) list -> thm -> thm list list -> thm list list
-    -> theory -> string list * theory
-  val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
-    -> string list option -> term list -> theory -> Proof.state
-  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
+  val derive_datatype_props : config -> string list -> descr list -> (string * sort) list ->
+    thm -> thm list list -> thm list list -> theory -> string list * theory
+  val rep_datatype : config -> (string list -> Proof.context -> Proof.context) ->
+    term list -> theory -> Proof.state
+  val rep_datatype_cmd : string list -> theory -> Proof.state
   val get_info : theory -> string -> info option
   val the_info : theory -> string -> info
-  val the_descr : theory -> string list
-    -> descr * (string * sort) list * string list
-      * string * (string list * string list) * (typ list * typ list)
+  val the_descr : theory -> string list ->
+    descr * (string * sort) list * string list * string *
+    (string list * string list) * (typ list * typ list)
   val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
   val all_distincts : theory -> typ list -> thm list list
   val get_constrs : theory -> string -> (string * typ) list option
   val get_all : theory -> info Symtab.table
   val info_of_constr : theory -> string * typ -> info option

         error ("Type constructors " ^ commas_quote raw_tycos ^
           " do not belong exhaustively to one mutual recursive datatype");
 
     val (Ts, Us) = (pairself o map) Type protoTs;
 
-    val names = map Long_Name.base_name (the_default tycos (#alt_names info));
+    val names = map Long_Name.base_name tycos;
     val (auxnames, _) =
       Name.make_context names
       |> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us;
     val prefix = space_implode "_" names;
 

   type T = Datatype_Aux.config * string list;
   val eq: T * T -> bool = eq_snd (op =);
 );
 fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
 
-fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
+fun make_dt_info descr sorts induct inducts rec_names rec_rewrites
     (index, (((((((((((_, (tname, _, _))), inject), distinct),
       exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
         (split, split_asm))) =
   (tname,
    {index = index,
-    alt_names = alt_names,
     descr = descr,
     sorts = sorts,
     inject = inject,
     distinct = distinct,
     induct = induct,

     case_cong = case_cong,
     weak_case_cong = weak_case_cong,
     split = split,
     split_asm = split_asm});
 
-fun derive_datatype_props config dt_names alt_names descr sorts
+fun derive_datatype_props config dt_names descr sorts
     induct inject distinct thy1 =
   let
     val thy2 = thy1 |> Theory.checkpoint;
     val flat_descr = flat descr;
-    val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+    val new_type_names = map Long_Name.base_name dt_names;
     val _ =
       Datatype_Aux.message config
         ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
 
     val (exhaust, thy3) =

       Datatype_Abs_Proofs.prove_split_thms
         config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
 
     val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct;
     val dt_infos = map_index
-      (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
+      (make_dt_info flat_descr sorts induct inducts rec_names rec_rewrites)
       (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
         case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
     val dt_names = map fst dt_infos;
     val prfx = Binding.qualify true (space_implode "_" new_type_names);
     val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;

 
 
 
 (** declare existing type as datatype **)
 
-fun prove_rep_datatype config dt_names alt_names descr sorts
-    raw_inject half_distinct raw_induct thy1 =
+fun prove_rep_datatype config dt_names descr sorts raw_inject half_distinct raw_induct thy1 =
   let
     val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
-    val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+    val new_type_names = map Long_Name.base_name dt_names;
     val prfx = Binding.qualify true (space_implode "_" new_type_names);
     val (((inject, distinct), [induct]), thy2) =
       thy1
       |> Datatype_Aux.store_thmss "inject" new_type_names raw_inject
       ||>> Datatype_Aux.store_thmss "distinct" new_type_names raw_distinct
       ||>> Global_Theory.add_thms
         [((prfx (Binding.name "induct"), raw_induct),
           [mk_case_names_induct descr])];
   in
     thy2
-    |> derive_datatype_props config dt_names alt_names [descr] sorts
-         induct inject distinct
+    |> derive_datatype_props config dt_names [descr] sorts induct inject distinct
  end;
 
-fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
+fun gen_rep_datatype prep_term config after_qed raw_ts thy =
   let
     val ctxt = Proof_Context.init_global thy;
 
     fun constr_of_term (Const (c, T)) = (c, T)
       | constr_of_term t = error ("Not a constant: " ^ Syntax.string_of_term ctxt t);

         val [[[raw_induct]], raw_inject, half_distinct] =
           unflat rules (map Drule.zero_var_indexes_list raw_thms);
             (*FIXME somehow dubious*)
       in
         Proof_Context.background_theory_result  (* FIXME !? *)
-          (prove_rep_datatype config dt_names alt_names descr vs
-            raw_inject half_distinct raw_induct)
+          (prove_rep_datatype config dt_names descr vs raw_inject half_distinct raw_induct)
         #-> after_qed
       end;
   in
     ctxt
     |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))

 
 (* outer syntax *)
 
 val _ =
   Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
-    (Scan.option (Parse.$$$ "(" |-- Scan.repeat1 Parse.name --| Parse.$$$ ")") --
-      Scan.repeat1 Parse.term
-      >> (fn (alt_names, ts) =>
-          Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
+    (Scan.repeat1 Parse.term >> (fn ts =>
+      Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd ts)));
 
 
 open Datatype_Aux;
 
 end;