src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
changeset 53918 0fc622be0185
parent 53909 7c10e75e62b3
child 53924 b19d300db73b
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 13:42:14 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 13:51:08 2013 +0200
@@ -398,7 +398,7 @@
     val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
   in
     (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #collapses ctr_sugars,
-     map #split ctr_sugars, map #split_asm ctr_sugars)
+     maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
   end;
 
 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;