# HG changeset patch
# User blanchet
# Date 1375797023 -7200
# Node ID 79f5e137779a1ca66961fd8d4ac6348a4673dd68
# Parent  cca9e958da5cbc5c768653b76f9c2d26a5450245
tuning

diff -r cca9e958da5c -r 79f5e137779a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Aug 06 15:50:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Aug 06 15:50:23 2013 +0200
@@ -671,7 +671,7 @@
   end;
 
 fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
-      [(unfold_args as (pgss, crgsss), _), (corec_args as (phss, cshsss), _)])
+      coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
     dtor_coinducts dtor_ctors dtor_coiter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss mss ns
     ctr_defss ctr_sugars coiterss coiter_defss export_args lthy =
   let
@@ -801,7 +801,7 @@
     fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
 
     val fcoiterss' as [gunfolds, hcorecs] =
-      map2 (fn (pfss, _) => map (lists_bmoc pfss)) [unfold_args, corec_args] coiterss';
+      map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss';
 
     val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) =
       let