# HG changeset patch
# User blanchet
# Date 1376671015 -7200
# Node ID e5fa456890b4bcd7791a752802c590c3a494d415
# Parent  7dd103c29f9d33a7f7021aa7370b67f43b3fe1c6
tuning

diff -r 7dd103c29f9d -r e5fa456890b4 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 18:14:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Aug 16 18:36:55 2013 +0200
@@ -219,10 +219,9 @@
 
 fun mk_co_iter thy fp fpT Cs t =
   let
-    val (binders, body) = strip_type (fastype_of t);
-    val (f_Cs, prebody) = split_last binders;
-    val fpT0 = if fp = Least_FP then prebody else body;
-    val Cs0 = distinct (op =) (map (if fp = Least_FP then body_type else domain_type) f_Cs);
+    val (f_Cs, Type (_, [prebody, body])) = strip_fun_type (fastype_of t);
+    val fpT0 = fp_case fp prebody body;
+    val Cs0 = distinct (op =) (map (fp_case fp body_type domain_type) f_Cs);
     val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs);
   in
     Term.subst_TVars rho t
@@ -239,7 +238,7 @@
     map (Term.subst_TVars rho) ts0
   end;
 
-val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
+val mk_fp_iter_fun_types = binder_fun_types o fastype_of;
 
 fun unzip_recT Cs (T as Type (@{type_name prod}, Ts as [_, U])) =
     if member (op =) Cs U then Ts else [T]
@@ -1444,8 +1443,8 @@
         kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~
         sel_bindingsss ~~ raw_sel_defaultsss)
       |> wrap_types_etc
-      |> (if fp = Least_FP then derive_and_note_induct_iters_thms_for_types
-          else derive_and_note_coinduct_coiters_thms_for_types);
+      |> fp_case fp derive_and_note_induct_iters_thms_for_types
+           derive_and_note_coinduct_coiters_thms_for_types;
 
     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
       co_prefix fp ^ "datatype"));
diff -r 7dd103c29f9d -r e5fa456890b4 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Aug 16 18:14:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Aug 16 18:36:55 2013 +0200
@@ -193,8 +193,9 @@
 open BNF_Util
 
 datatype fp_kind = Least_FP | Greatest_FP;
-fun fp_case Least_FP f1 _ = f1
-  | fp_case Greatest_FP _ f2 = f2;
+
+fun fp_case Least_FP l _ = l
+  | fp_case Greatest_FP _ g = g;
 
 type fp_result =
   {Ts: typ list,
diff -r 7dd103c29f9d -r e5fa456890b4 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:14:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Aug 16 18:36:55 2013 +0200
@@ -78,6 +78,7 @@
   val binder_fun_types: typ -> typ list
   val body_fun_type: typ -> typ
   val num_binder_types: typ -> int
+  val strip_fun_type: typ -> typ list * typ
   val strip_typeN: int -> typ -> typ list * typ
 
   val mk_predT: typ list -> typ