# HG changeset patch
# User blanchet
# Date 1410177782 -7200
# Node ID 61b852f90161b4643ba599a772a64461a5ef4fc5
# Parent  a92acec845a716b0d257477c16e92e9ae9b19a8f
improved 'datatype_compat' further for recursion through functions

diff -r a92acec845a7 -r 61b852f90161 src/HOL/Nominal/Examples/CK_Machine.thy
--- a/src/HOL/Nominal/Examples/CK_Machine.thy	Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Mon Sep 08 14:03:02 2014 +0200
@@ -583,14 +583,5 @@
 by (induct \<Gamma>\<equiv>"[]::tctx" t T)
    (auto dest!: canonical_tINT intro!: cbv.intros gr0I)
 
-end    
-   
-
-
+end
 
-  
-
-  
-  
-
-
diff -r a92acec845a7 -r 61b852f90161 src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy	Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Nominal/Examples/W.thy	Mon Sep 08 14:03:02 2014 +0200
@@ -46,7 +46,7 @@
     Var "var"
   | App "trm" "trm" 
   | Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
-  | Let "\<guillemotleft>var\<guillemotright>trm" "trm" 
+  | Let "\<guillemotleft>var\<guillemotright>trm" "trm"
 
 abbreviation
   LetBe :: "var \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" ("Let _ be _ in _" [100,100,100] 100)
diff -r a92acec845a7 -r 61b852f90161 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 08 14:03:02 2014 +0200
@@ -183,6 +183,10 @@
     ((inducts', induct', recs', rec'_thmss), lthy')
   end;
 
+fun body_rec_indices (Old_Datatype_Aux.DtRec kk) = [kk]
+  | body_rec_indices (Old_Datatype_Aux.DtType (@{type_name fun}, [_, D])) = body_rec_indices D
+  | body_rec_indices _ = [];
+
 fun reindex_desc desc =
   let
     val kks = map fst desc;
@@ -259,22 +263,19 @@
       split_list (flat (map_index (fn (i, descr) => map (pair i) descr)
         (maps cliquify_descr descrs)));
 
-    val dest_dtyp = Old_Datatype_Aux.typ_of_dtyp descr;
-
     val fpTs' = Old_Datatype_Aux.get_rec_types descr;
     val nn = length fpTs';
 
     val fp_sugars = map (lfp_sugar_of o fst o dest_Type) fpTs';
-    val ctrXs_Tsss = map (map (map dest_dtyp o snd) o #3 o snd) descr;
-    val kkssss =
-      map (map (map (fn Old_Datatype_Aux.DtRec kk => [kk] | _ => []) o snd) o #3 o snd) descr;
+    val ctr_Tsss = map (map (map (Old_Datatype_Aux.typ_of_dtyp descr) o snd) o #3 o snd) descr;
+    val kkssss = map (map (map body_rec_indices o snd) o #3 o snd) descr;
 
     val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1);
 
     fun apply_comps n kk =
       mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk);
 
-    val callssss = map2 (map2 (map2 (map o apply_comps o num_binder_types))) ctrXs_Tsss kkssss;
+    val callssss = map2 (map2 (map2 (map o apply_comps o num_binder_types))) ctr_Tsss kkssss;
 
     val b_names = Name.variant_list [] (map base_name_of_typ fpTs');
     val compat_b_names = map (prefix compat_N) b_names;