diff -r 83392f9d303f -r aeb1e44fbc19 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Oct 15 23:28:10 2009 +0200
@@ -329,7 +329,7 @@
       REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
       REPEAT (FIRST
         [atac 1,
-         resolve_tac (List.concat (map mk_mono monos) @ get_monos ctxt) 1,
+         resolve_tac (maps mk_mono monos @ get_monos ctxt) 1,
          etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));