# HG changeset patch
# User blanchet
# Date 1367235774 -7200
# Node ID ca201253e7bbd050109b4f0e6d9fd68d13f98ac3
# Parent  329c62d9997992413f20c4412397083d6f768d77
tuning

diff -r 329c62d99979 -r ca201253e7bb src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:41:34 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:42:54 2013 +0200
@@ -20,9 +20,8 @@
     int list -> term list -> term list list -> term list list -> term list list list list ->
     term list list list list -> term list list -> term list list list list ->
     term list list list list -> term list list -> thm list list ->
-    (term list * term list list * thm * 'a * 'b * 'c * thm list list * thm list
-       * thm list list) list ->
-    term list -> term list -> thm list -> thm list -> Proof.context ->
+    BNF_Ctr_Sugar.ctr_wrap_result list -> term list -> term list -> thm list -> thm list ->
+    Proof.context ->
     (thm * thm list * thm * thm list * Args.src list) * (thm list list * thm list list * 'e list)
     * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
     * (thm list list * thm list list * Args.src list) *