src/HOL/Tools/inductive_realizer.ML
changeset 31783 cfbe9609ceb1
parent 31781 861e675f01e6
child 31784 bd3486c57ba3
--- 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) =>