# HG changeset patch
# User blanchet
# Date 1367955460 -7200
# Node ID a6b963bc46f049a7c11c476864a0cf0fd013b6a6
# Parent  6c425d450a8c4ca3ec7e4b2ee22b3f7bd36b3dc1
removed dead argument

diff -r 6c425d450a8c -r a6b963bc46f0 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 21:09:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 21:37:40 2013 +0200
@@ -29,8 +29,8 @@
   val exists_subtype_in: typ list -> typ -> bool
   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
   val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
-  val mk_un_fold_co_rec_prelims: bool -> typ list -> typ list -> typ list -> int list ->
-    int list list -> term list -> term list -> Proof.context ->
+  val mk_un_fold_co_rec_prelims: bool -> typ list -> typ list -> int list -> int list list ->
+    term list -> term list -> Proof.context ->
     (term list * term list * ((term list list * typ list list * term list list list)
        * (term list list * typ list list * term list list list)) option
      * (term list * term list list
@@ -56,7 +56,7 @@
     (term * term * thm * thm) * Proof.context
   val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm ->
     thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
-    typ list -> term list list -> thm list list -> term list -> term list -> thm list -> thm list ->
+    term list list -> thm list list -> term list -> term list -> thm list -> thm list ->
     local_theory ->
     (thm * thm list * Args.src list) * (thm list list * Args.src list)
     * (thm list list * Args.src list)
@@ -349,7 +349,7 @@
     ((cs, cpss, (unfold_args, unfold_types), (corec_args, corec_types)), lthy)
   end;
 
-fun mk_un_fold_co_rec_prelims lfp fpTs As Cs ns mss fp_folds0 fp_recs0 lthy =
+fun mk_un_fold_co_rec_prelims lfp fpTs Cs ns mss fp_folds0 fp_recs0 lthy =
   let
     val (fp_folds, fp_fold_fun_Ts) = mk_fp_iters lthy lfp fpTs Cs fp_folds0;
     val (fp_recs, fp_rec_fun_Ts) = mk_fp_iters lthy lfp fpTs Cs fp_recs0;
@@ -549,7 +549,7 @@
   end;
 
 fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_folds0 ctor_recs0 ctor_induct ctor_fold_thms
-    ctor_rec_thms nesting_bnfs nested_bnfs fpTs Cs As ctrss ctr_defss folds recs fold_defs rec_defs
+    ctor_rec_thms nesting_bnfs nested_bnfs fpTs Cs ctrss ctr_defss folds recs fold_defs rec_defs
     lthy =
   let
     val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
@@ -1128,7 +1128,7 @@
     val mss = map (map length) ctr_Tsss;
 
     val ((fp_folds, fp_recs, fold_rec_args_types, unfold_corec_args_types), lthy) =
-      mk_un_fold_co_rec_prelims lfp fpTs As Cs ns mss fp_folds0 fp_recs0 lthy;
+      mk_un_fold_co_rec_prelims lfp fpTs Cs ns mss fp_folds0 fp_recs0 lthy;
 
     fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
             fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
@@ -1344,7 +1344,7 @@
         val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
              (rec_thmss, rec_attrs)) =
           derive_induct_fold_rec_thms_for_types pre_bnfs fp_folds0 fp_recs0 fp_induct fp_fold_thms
-            fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As ctrss ctr_defss folds recs fold_defs
+            fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs ctrss ctr_defss folds recs fold_defs
             rec_defs lthy;
 
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;