simpler code
authorblanchet
Mon, 02 Dec 2013 20:31:54 +0100
changeset 55987689398f0953f
parent 55986 985f8b49c050
child 55988 62fb5af93fe2
simpler code
src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
     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;