Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuning
authorblanchet
Mon, 29 Apr 2013 13:42:54 +0200
changeset 51813 ca201253e7bb
parent 51812 329c62d99979
child 51814 8b89afea27e7
tuning
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML file | annotate | diff | comparison | revisions 
--- 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) *
isabelle