src/HOL/Tools/inductive_realizer.ML
changeset 31783 cfbe9609ceb1
parent 31781 861e675f01e6
child 31784 bd3486c57ba3
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 14:51:21 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 15:32:34 2009 +0200
     1.3 @@ -305,15 +305,17 @@
     1.4  
     1.5      (** datatype representing computational content of inductive set **)
     1.6  
     1.7 -    val ((dummies, (dt_names_rules)), thy2) =
     1.8 +    val ((dummies, some_dt_names), thy2) =
     1.9        thy1
    1.10        |> add_dummies (Datatype.add_datatype
    1.11             { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
    1.12             (map (pair false) dts) []
    1.13        ||> Extraction.add_typeof_eqns_i ty_eqs
    1.14        ||> Extraction.add_realizes_eqns_i rlz_eqs;
    1.15 -    val rec_thms = these (Option.map (#rec_thms o snd) dt_names_rules);
    1.16 -    val case_thms = these (Option.map (#case_thms o snd) dt_names_rules);
    1.17 +    val dt_names = these some_dt_names;
    1.18 +    val case_thms = map (#case_rewrites o Datatype.the_datatype thy2) dt_names;
    1.19 +    val rec_thms = if null dt_names then []
    1.20 +      else (#rec_rewrites o Datatype.the_datatype thy2) (hd dt_names);
    1.21      val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
    1.22        HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
    1.23      val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>