# HG changeset patch
# User blanchet
# Date 1410177781 -7200
# Node ID a456b2c0349102d0c778beed5170fc3f7cbf8872
# Parent  2e771e0e50ee1fdbb7b16603401d50537434d64c
tuning

diff -r 2e771e0e50ee -r a456b2c03491 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -81,7 +81,7 @@
     int list list -> term ->
     typ list list
     * (typ list list list list * typ list list list * typ list list list list * typ list)
-  val define_co_rec_as: BNF_Util.fp_kind -> typ -> typ list -> binding -> term -> local_theory ->
+  val define_co_rec_as: BNF_Util.fp_kind -> typ list -> typ -> binding -> term -> local_theory ->
     (term * thm) * local_theory
   val define_rec:
     typ list list * typ list list list list * term list list * term list list list list ->
@@ -523,7 +523,7 @@
     Term.lambda c (mk_IfN absT cps ts)
   end;
 
-fun define_co_rec_as fp fpT Cs b rhs lthy0 =
+fun define_co_rec_as fp Cs fpT b rhs lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
@@ -548,7 +548,7 @@
     val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec)
       |>> map domain_type ||> domain_type;
   in
-    define_co_rec_as Least_FP fpT Cs (mk_binding recN)
+    define_co_rec_as Least_FP Cs fpT (mk_binding recN)
       (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
          map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
              mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
@@ -561,7 +561,7 @@
     val nn = length fpTs;
     val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
   in
-    define_co_rec_as Greatest_FP fpT Cs (mk_binding corecN)
+    define_co_rec_as Greatest_FP Cs fpT (mk_binding corecN)
       (fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec,
          map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
   end;