src/HOL/Codatatype/Tools/bnf_sugar.ML

--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 16:07:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 16:07:06 2012 +0200
@@ -36,9 +36,11 @@
 
 val default_name = @{binding _};
 
+fun pad_list x n xs = xs @ replicate (n - length xs) x;
+
 fun mk_half_pairss' _ [] = []
-  | mk_half_pairss' pad (y :: ys) =
-    pad @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: pad) ys);
+  | mk_half_pairss' indent (y :: ys) =
+    indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys);
 
 fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
 
@@ -86,27 +88,21 @@
 
     val ms = map length ctr_Tss;
 
-    val raw_disc_names' =
-      raw_disc_names @ replicate (n - length raw_disc_names) default_name;
-    val raw_sel_namess' =
-      map2 (fn m => fn sels => sels @ replicate (m - length sels) default_name)
-        ms (raw_sel_namess @ replicate (n - length raw_sel_namess) []);
-
     val disc_names =
-      map2 (fn ctr => fn disc =>
+      pad_list default_name n raw_disc_names
+      |> map2 (fn ctr => fn disc =>
         if Binding.eq_name (disc, default_name) then
           Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr)))
         else
-          disc) ctrs0 raw_disc_names';
+          disc) ctrs0;
+
     val sel_namess =
-      map2 (fn ctr => fn sels =>
-        let val m = length sels in
-          map2 (fn l => fn sel =>
-            if Binding.eq_name (sel, default_name) then
-              Binding.name (mk_un_N m l (Long_Name.base_name (name_of_ctr ctr)))
-            else
-              sel) (1 upto m) sels
-        end) ctrs0 raw_sel_namess';
+      pad_list [] n raw_sel_namess
+      |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
+        if Binding.eq_name (sel, default_name) then
+          Binding.name (mk_un_N m l (Long_Name.base_name (name_of_ctr ctr)))
+        else
+          sel) (1 upto m) o pad_list default_name m) ctrs0 ms;
 
     fun mk_caseof Ts T =
       let val (binders, body) = strip_type (fastype_of caseof0) in