# HG changeset patch
# User blanchet
# Date 1367236334 -7200
# Node ID efacb9b9986569b5abb0056635b7bd6a14c2c0c1
# Parent  8b89afea27e7a770ba2ab14bc8f63de09f598a0d
tune signatures

diff -r 8b89afea27e7 -r efacb9b99865 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:47:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:52:14 2013 +0200
@@ -7,14 +7,13 @@
 
 signature BNF_FP_DEF_SUGAR =
 sig
-  val derive_induct_fold_rec_thms_for_types: int -> BNF_Def.BNF list -> thm -> thm list ->
-    thm list -> BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list ->
-    typ list list list -> int list list -> int list -> term list list -> term list list ->
-    term list list -> term list list list -> thm list list -> term list -> term list -> thm list ->
-    thm list -> Proof.context ->
+  val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> thm -> thm list -> thm list ->
+    BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list -> typ list list list ->
+    int list list -> int list -> term list list -> term list list -> term list list -> term list
+    list list -> thm list list -> term list -> term list -> thm list -> thm list -> Proof.context ->
     (thm * thm list * Args.src list) * (thm list list * Args.src list)
       * (thm list list * Args.src list)
-  val derive_coinduct_unfold_corec_thms_for_types: Proof.context -> Proof.context -> int ->
+  val derive_coinduct_unfold_corec_thms_for_types: Proof.context -> Proof.context ->
     BNF_Def.BNF list -> thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.BNF list ->
     BNF_Def.BNF list -> typ list -> typ list -> typ list -> int list list -> int list list ->
     int list -> term list -> term list list -> term list list -> term list list list list ->
@@ -199,10 +198,12 @@
     val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
   in Term.list_comb (rel, map build_arg Ts') end;
 
-fun derive_induct_fold_rec_thms_for_types nn pre_bnfs ctor_induct ctor_fold_thms ctor_rec_thms
+fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_induct ctor_fold_thms ctor_rec_thms
     nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
     fold_defs rec_defs lthy =
   let
+    val nn = length pre_bnfs;
+
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
@@ -352,11 +353,13 @@
      (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
   end;
 
-fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs dtor_coinduct
+fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy pre_bnfs dtor_coinduct
     dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs
     As kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
     unfolds corecs unfold_defs corec_defs lthy =
   let
+    val nn = length pre_bnfs;
+
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
@@ -529,7 +532,8 @@
             dtor_corec_thms pre_map_defs ctr_defss;
 
         fun prove goal tac =
-          Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation;
+          Goal.prove_sorry lthy [] [] goal (tac o #context)
+          |> Thm.close_derivation;
 
         val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
         val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
@@ -1208,7 +1212,7 @@
         val ((induct_thm, induct_thms, induct_attrs),
              (fold_thmss, fold_attrs),
              (rec_thmss, rec_attrs)) =
-          derive_induct_fold_rec_thms_for_types nn pre_bnfs fp_induct fp_fold_thms fp_rec_thms
+          derive_induct_fold_rec_thms_for_types pre_bnfs fp_induct fp_fold_thms fp_rec_thms
             nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
             fold_defs rec_defs lthy;
 
@@ -1240,7 +1244,7 @@
              (disc_unfold_thmss, disc_corec_thmss, disc_corec_like_attrs),
              (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_corec_like_iff_attrs),
              (sel_unfold_thmss, sel_corec_thmss, sel_corec_like_attrs)) =
-          derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs fp_induct
+          derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy pre_bnfs fp_induct
             fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As
             kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
             unfolds corecs unfold_defs corec_defs lthy;