made datatype realizer plugin work for new-style datatypes with no nesting

--- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -16,6 +16,9 @@
   "datatype_compat" :: thy_decl
 begin
 
+ML {* proofs := 2 *} (*###*)
+ML {* Proofterm.proofs_enabled () *}
+
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
   by blast
 

--- a/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -7,12 +7,15 @@
 
 signature OLD_DATATYPE_REALIZER =
 sig
+  val realizer_plugin: string
   val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
 end;
 
 structure Old_Datatype_Realizer : OLD_DATATYPE_REALIZER =
 struct
 
+val realizer_plugin = "realizer";
+
 fun subsets i j =
   if i <= j then
     let val is = subsets (i+1) j
@@ -155,7 +158,10 @@
           (map Logic.unvarify_global ivs1 @ filter_out is_unit
               (map (head_of o strip_abs_body) rec_fns)) r);
 
-  in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
+  in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end
+  (* Nested new-style datatypes are not supported (unless they are registered via
+     "datatype_compat"). *)
+  handle Old_Datatype_Aux.Datatype => thy;
 
 fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
   let
@@ -230,7 +236,7 @@
   else
     let
       val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
-      val infos = map (Old_Datatype_Data.the_info thy) names;
+      val infos = map (BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Unfold_Nesting) names;
       val info :: _ = infos;
     in
       thy
@@ -238,6 +244,7 @@
       |> fold_rev make_casedists infos
     end;
 
-val _ = Theory.setup (Old_Datatype_Data.interpretation add_dt_realizers);
+val _ = Theory.setup (BNF_LFP_Compat.interpretation realizer_plugin BNF_LFP_Compat.Unfold_Nesting
+  add_dt_realizers);
 
 end;

--- a/src/HOL/Tools/inductive_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -521,4 +521,3 @@
     "add realizers for inductive set";
 
 end;
-