src/HOL/Tools/Datatype/datatype.ML
changeset 32719 36cae240b46c
parent 32718 45929374f1bd
child 32720 fc32e6771749
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:19:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:34:50 2009 +0200
     1.3 @@ -347,24 +347,14 @@
     1.4  
     1.5  (** declare existing type as datatype **)
     1.6  
     1.7 -fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
     1.8 +fun prove_rep_datatype (config : config) dt_names alt_names descr sorts induct inject half_distinct thy =
     1.9    let
    1.10 -    val ((_, [induct']), _) =
    1.11 -      Variable.importT [induct] (Variable.thm_context induct);
    1.12 -
    1.13 -    fun err t = error ("Ill-formed predicate in induction rule: " ^
    1.14 -      Syntax.string_of_term_global thy t);
    1.15 -
    1.16 -    fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
    1.17 -          ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
    1.18 -      | get_typ t = err t;
    1.19 -    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
    1.20 -
    1.21 -    val dt_info = get_all thy;
    1.22  
    1.23      val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
    1.24 +
    1.25 +    val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
    1.26      val (case_names_induct, case_names_exhausts) =
    1.27 -      (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
    1.28 +      (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
    1.29  
    1.30      val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    1.31  
    1.32 @@ -372,7 +362,7 @@
    1.33        DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
    1.34          case_names_exhausts;
    1.35      val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
    1.36 -      config new_type_names [descr] sorts dt_info inject distinct
    1.37 +      config new_type_names [descr] sorts (get_all thy) inject distinct
    1.38        (Simplifier.theory_context thy2 dist_ss) induct thy2;
    1.39      val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
    1.40        config new_type_names [descr] sorts reccomb_names rec_thms thy3;
    1.41 @@ -451,7 +441,7 @@
    1.42      val cs = map (apsnd (map norm_constr)) raw_cs;
    1.43      val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
    1.44        o fst o strip_type;
    1.45 -    val new_type_names = map Long_Name.base_name (the_default (map fst cs) alt_names);
    1.46 +    val dt_names = map fst cs;
    1.47  
    1.48      fun mk_spec (i, (tyco, constr)) = (i, (tyco,
    1.49        map (DtTFree o fst) vs,
    1.50 @@ -469,7 +459,7 @@
    1.51              (*FIXME somehow dubious*)
    1.52        in
    1.53          ProofContext.theory_result
    1.54 -          (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts)
    1.55 +          (prove_rep_datatype config dt_names alt_names descr vs induct injs half_distincts)
    1.56          #-> after_qed
    1.57        end;
    1.58    in