--- a/src/HOL/BNF/Tools/bnf_wrap.ML Thu Apr 25 08:56:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML Thu Apr 25 09:25:50 2013 +0200
@@ -121,7 +121,9 @@
val sel_defaultss =
pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
- val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0));
+ val case0T = fastype_of case0;
+ val Type (dataT_name, As0) =
+ domain_type (snd (strip_typeN (length (binder_types case0T) - 1) case0T));
val data_b = Binding.qualified_name dataT_name;
val data_b_name = Binding.name_of data_b;