# HG changeset patch
# User blanchet
# Date 1409581067 -7200
# Node ID 8119d6e5d02460814ec2e2594ad6c6570a46f115
# Parent  0a58bff4939d5c95720dbede77d0dc616be3f530
tuning

diff -r 0a58bff4939d -r 8119d6e5d024 src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/BNF_LFP.thy	Mon Sep 01 16:17:47 2014 +0200
@@ -193,6 +193,30 @@
 ML_file "Tools/BNF/bnf_lfp_compat.ML"
 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
 
+datatype_new 'a l = N | C 'a "'a l"
+datatype_compat l
+
+datatype_new 'a m = P | D 'a "'a m l"
+and 'a n = Q
+datatype_compat l
+datatype_compat m n
+
+declare [[ML_exception_trace]]
+ML \<open>
+BNF_LFP_Compat.Datatype_Data.get_all @{theory} true
+|> Symtab.dest |> (fn xs => nth xs 4) |> snd |> #descr
+\<close>
+
+ML \<open>
+BNF_LFP_Compat.Datatype_Data.get_info @{theory} true @{type_name m}
+|> the |> #descr
+\<close>
+
+
+ML \<open>
+BNF_FP_Def_Sugar.fp_sugars_of @{context} |> tl |> hd |> #fp_res_index 
+\<close>
+
 hide_fact (open) id_transfer
 
 end
diff -r 0a58bff4939d -r 8119d6e5d024 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -2,7 +2,10 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2013, 2014
 
-Compatibility layer with the old datatype package.
+Compatibility layer with the old datatype package. Parly based on:
+
+    Title:      HOL/Tools/Old_Datatype/old_datatype_data.ML
+    Author:     Stefan Berghofer, TU Muenchen
 *)
 
 signature BNF_LFP_COMPAT =
@@ -239,16 +242,18 @@
 
 fun get_constrs thy unfold_nesting T_name =
   try (the_spec thy unfold_nesting) T_name
-  |> Option.map (fn (Ts, ctrs) =>
-      let
-        fun subst (v, S) = TVar ((v, 0), S);
-        fun subst_ty (TFree v) = subst v
-          | subst_ty ty = ty;
-        val dataT = Type (T_name, map subst Ts);
-        fun mk_ctr_typ Ts = map (Term.map_atyps subst_ty) Ts ---> dataT;
-      in
-        map (apsnd mk_ctr_typ) ctrs
-      end);
+  |> Option.map (fn (tfrees, ctrs) =>
+    let
+      fun varify_tfree (s, S) = TVar ((s, 0), S);
+      fun varify_typ (TFree x) = varify_tfree x
+        | varify_typ T = T;
+
+      val dataT = Type (T_name, map varify_tfree tfrees);
+
+      fun mk_ctr_typ Ts = map (Term.map_atyps varify_typ) Ts ---> dataT;
+    in
+      map (apsnd mk_ctr_typ) ctrs
+    end);
 
 fun interpretation f thy = Old_Datatype_Data.interpretation f thy;