--- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 23 14:51:21 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 23 15:32:34 2009 +0200
@@ -305,15 +305,17 @@
(** datatype representing computational content of inductive set **)
- val ((dummies, (dt_names_rules)), thy2) =
+ val ((dummies, some_dt_names), thy2) =
thy1
|> add_dummies (Datatype.add_datatype
{ strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
(map (pair false) dts) []
||> Extraction.add_typeof_eqns_i ty_eqs
||> Extraction.add_realizes_eqns_i rlz_eqs;
- val rec_thms = these (Option.map (#rec_thms o snd) dt_names_rules);
- val case_thms = these (Option.map (#case_thms o snd) dt_names_rules);
+ val dt_names = these some_dt_names;
+ val case_thms = map (#case_rewrites o Datatype.the_datatype thy2) dt_names;
+ val rec_thms = if null dt_names then []
+ else (#rec_rewrites o Datatype.the_datatype thy2) (hd dt_names);
val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>