# HG changeset patch
# User blanchet
# Date 1514905263 -3600
# Node ID adaf279ce67b2b612bb7aa6f20949bb9b81e362c
# Parent  9301e197a47b38441fda88e1b8805061c9672ddb
ported inductive realizer to new datatype package

diff -r 9301e197a47b -r adaf279ce67b src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jan 02 15:01:06 2018 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jan 02 16:01:03 2018 +0100
@@ -246,7 +246,7 @@
       thy
       |> f (map snd dts)
       |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
-    handle Old_Datatype_Aux.Datatype_Empty name' =>
+    handle BNF_FP_Util.EMPTY_DATATYPE name' =>
       let
         val name = Long_Name.base_name name';
         val dname = singleton (Name.variant_list used) "Dummy";
@@ -308,15 +308,15 @@
 
     val ((dummies, some_dt_names), thy2) =
       thy1
-      |> add_dummies (Old_Datatype.add_datatype {strict = false, quiet = false})
+      |> add_dummies (BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Kill_Type_Args])
         (map (pair false) dts) []
       ||> Extraction.add_typeof_eqns_i ty_eqs
       ||> Extraction.add_realizes_eqns_i rlz_eqs;
     val dt_names = these some_dt_names;
-    val case_thms = map (#case_rewrites o Old_Datatype_Data.the_info thy2) dt_names;
+    val case_thms = map (#case_rewrites o BNF_LFP_Compat.the_info thy2 []) dt_names;
     val rec_thms =
       if null dt_names then []
-      else #rec_rewrites (Old_Datatype_Data.the_info thy2 (hd dt_names));
+      else #rec_rewrites (BNF_LFP_Compat.the_info 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 Thm.prop_of) rec_thms);
     val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>