ported TFL to mixture of old and new datatypes

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 01 19:28:00 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 01 19:57:48 2014 +0200
@@ -144,7 +144,7 @@
     | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
     | _ => raise CTERM ("no equation", [ct]))
 
-  fun get_constrs thy (Type (n, _)) = these (Old_Datatype_Data.get_constrs thy n)
+  fun get_constrs thy (Type (n, _)) = these (BNF_LFP_Compat.get_constrs thy n)
     | get_constrs _ _ = []
 
   fun is_constr thy (n, T) =

--- a/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 01 19:28:00 2014 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 01 19:57:48 2014 +0200
@@ -24,7 +24,7 @@
                      Type(ty_str, _) => ty_str
                    | TFree(s,_)  => error ("Free type: " ^ s)
                    | TVar((s,i),_) => error ("Free variable: " ^ s)
-      val {induct, ...} = Old_Datatype_Data.the_info thy ty_str
+      val {induct, ...} = BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Keep_Nesting ty_str
     in
       cases_thm_of_induct_thm induct
     end;

--- a/src/HOL/Tools/TFL/tfl.ML	Mon Sep 01 19:28:00 2014 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon Sep 01 19:57:48 2014 +0200
@@ -435,7 +435,7 @@
        put_simpset HOL_basic_ss ctxt
           addsimps case_rewrites
           |> fold (Simplifier.add_cong o #case_cong_weak o snd)
-              (Symtab.dest (Old_Datatype_Data.get_all theory))
+              (Symtab.dest (BNF_LFP_Compat.get_all theory BNF_LFP_Compat.Keep_Nesting))
      val corollaries' = map (Simplifier.simplify case_simpset) corollaries
      val extract = Rules.CONTEXT_REWRITE_RULE
                      (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)

--- a/src/HOL/Tools/TFL/thry.ML	Mon Sep 01 19:28:00 2014 +0200
+++ b/src/HOL/Tools/TFL/thry.ML	Mon Sep 01 19:57:48 2014 +0200
@@ -58,20 +58,20 @@
  *---------------------------------------------------------------------------*)
 
 fun match_info thy dtco =
-  case (Old_Datatype_Data.get_info thy dtco,
-         Old_Datatype_Data.get_constrs thy dtco) of
-      (SOME { case_name, ... }, SOME constructors) =>
+  case (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco,
+         BNF_LFP_Compat.get_constrs thy dtco) of
+      (SOME {case_name, ... }, SOME constructors) =>
         SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
     | _ => NONE;
 
-fun induct_info thy dtco = case Old_Datatype_Data.get_info thy dtco of
+fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco of
         NONE => NONE
       | SOME {nchotomy, ...} =>
           SOME {nchotomy = nchotomy,
-                constructors = (map Const o the o Old_Datatype_Data.get_constrs thy) dtco};
+                constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco};
 
 fun extract_info thy =
- let val infos = map snd (Symtab.dest (Old_Datatype_Data.get_all thy))
+ let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Keep_Nesting))
  in {case_congs = map (mk_meta_eq o #case_cong) infos,
      case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
  end;