# HG changeset patch
# User blanchet
# Date 1386012714 -3600
# Node ID 689398f0953f3fb432f1f78d25bccf31274c5937
# Parent  985f8b49c050b2092c593b06004c947dc15f5eeb
simpler code

diff -r 985f8b49c050 -r 689398f0953f src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Dec 01 19:32:57 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Dec 02 20:31:54 2013 +0100
@@ -28,7 +28,8 @@
 structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
 struct
 
-fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
+fun indexe _ h = (h, h + 1);
+fun indexed xs = fold_map indexe xs;
 fun indexedd xss = fold_map indexed xss;
 fun indexeddd xsss = fold_map indexedd xsss;
 fun indexedddd xssss = fold_map indexeddd xssss;