# HG changeset patch
# User blanchet
# Date 1370002128 -7200
# Node ID c3f837d9253777a223f43369d977c0912070f679
# Parent  1d37d281645d989f23370bfab6052f085c19c912
tuning

diff -r 1d37d281645d -r c3f837d92537 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Fri May 31 12:28:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Fri May 31 14:08:48 2013 +0200
@@ -176,7 +176,7 @@
 
     val case0T = fastype_of case0;
     val Type (dataT_name, As0) =
-      domain_type (snd (strip_typeN (length (binder_types case0T) - 1) case0T));
+      domain_type (snd (strip_typeN (num_binder_types case0T - 1) case0T));
     val data_b = Binding.qualified_name dataT_name;
     val data_b_name = Binding.name_of data_b;
 
diff -r 1d37d281645d -r c3f837d92537 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri May 31 12:28:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri May 31 14:08:48 2013 +0200
@@ -70,6 +70,7 @@
   val retype_free: typ -> term -> term
   val nonzero_string_of_int: int -> string
 
+  val num_binder_types: typ -> int
   val strip_typeN: int -> typ -> typ list * typ
 
   val mk_predT: typ list -> typ
@@ -387,6 +388,11 @@
 
 (** Types **)
 
+(*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*)
+fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
+    1 + num_binder_types T2
+  | num_binder_types _ = 0
+
 fun strip_typeN 0 T = ([], T)
   | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T
   | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []);