1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Sun Dec 01 19:32:57 2013 +0100
1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Dec 02 20:31:54 2013 +0100
1.3 @@ -28,7 +28,8 @@
1.4 structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
1.5 struct
1.6
1.7 -fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
1.8 +fun indexe _ h = (h, h + 1);
1.9 +fun indexed xs = fold_map indexe xs;
1.10 fun indexedd xss = fold_map indexed xss;
1.11 fun indexeddd xsss = fold_map indexedd xsss;
1.12 fun indexedddd xssss = fold_map indexeddd xssss;