tuning
authorblanchet
Mon Apr 29 13:42:54 2013 +0200 (2013-04-29)
changeset 51813ca201253e7bb
parent 51812 329c62d99979
child 51814 8b89afea27e7
tuning
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:41:34 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:42:54 2013 +0200
     1.3 @@ -20,9 +20,8 @@
     1.4      int list -> term list -> term list list -> term list list -> term list list list list ->
     1.5      term list list list list -> term list list -> term list list list list ->
     1.6      term list list list list -> term list list -> thm list list ->
     1.7 -    (term list * term list list * thm * 'a * 'b * 'c * thm list list * thm list
     1.8 -       * thm list list) list ->
     1.9 -    term list -> term list -> thm list -> thm list -> Proof.context ->
    1.10 +    BNF_Ctr_Sugar.ctr_wrap_result list -> term list -> term list -> thm list -> thm list ->
    1.11 +    Proof.context ->
    1.12      (thm * thm list * thm * thm list * Args.src list) * (thm list list * thm list list * 'e list)
    1.13      * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
    1.14      * (thm list list * thm list list * Args.src list) *