Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51813 ca201253e7bb
parent 51811 1461426e2bf1
child 51814 8b89afea27e7 
--- 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