# HG changeset patch
# User haftmann
# Date 1254076490 -7200
# Node ID 36cae240b46cac5b25056ffb641f18ab9a969a3a
# Parent  45929374f1bda71b85b09ff7dc15591d8195b6bd
simplified rep_datatype

diff -r 45929374f1bd -r 36cae240b46c src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:19:56 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:34:50 2009 +0200
@@ -347,24 +347,14 @@
 
 (** declare existing type as datatype **)
 
-fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
+fun prove_rep_datatype (config : config) dt_names alt_names descr sorts induct inject half_distinct thy =
   let
-    val ((_, [induct']), _) =
-      Variable.importT [induct] (Variable.thm_context induct);
-
-    fun err t = error ("Ill-formed predicate in induction rule: " ^
-      Syntax.string_of_term_global thy t);
-
-    fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
-          ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
-      | get_typ t = err t;
-    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
-
-    val dt_info = get_all thy;
 
     val 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 (case_names_induct, case_names_exhausts) =
-      (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
+      (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
 
     val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
 
@@ -372,7 +362,7 @@
       DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
         case_names_exhausts;
     val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
-      config new_type_names [descr] sorts dt_info inject distinct
+      config new_type_names [descr] sorts (get_all thy) inject distinct
       (Simplifier.theory_context thy2 dist_ss) induct thy2;
     val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
       config new_type_names [descr] sorts reccomb_names rec_thms thy3;
@@ -451,7 +441,7 @@
     val cs = map (apsnd (map norm_constr)) raw_cs;
     val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
       o fst o strip_type;
-    val new_type_names = map Long_Name.base_name (the_default (map fst cs) alt_names);
+    val dt_names = map fst cs;
 
     fun mk_spec (i, (tyco, constr)) = (i, (tyco,
       map (DtTFree o fst) vs,
@@ -469,7 +459,7 @@
             (*FIXME somehow dubious*)
       in
         ProofContext.theory_result
-          (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts)
+          (prove_rep_datatype config dt_names alt_names descr vs induct injs half_distincts)
         #-> after_qed
       end;
   in