# HG changeset patch
# User blanchet
# Date 1366805676 -7200
# Node ID e5ce85418346a43d18a711781a792144f8d62cb1
# Parent  587bba4254302577d853bd53b2db0e477562b811
killed dead code

diff -r 587bba425430 -r e5ce85418346 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 14:05:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 14:14:36 2013 +0200
@@ -276,14 +276,6 @@
     in (x :: xs, acc'') end
   | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
-fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc)
-  | fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc =
-    let
-      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc;
-      val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc';
-    in (x :: xs, acc'') end
-  | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
 fun fold_map8 _ [] [] [] [] [] [] [] [] acc = ([], acc)
   | fold_map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
       acc =