diff -r 83392f9d303f -r aeb1e44fbc19 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/recdef.ML	Thu Oct 15 23:28:10 2009 +0200
@@ -209,7 +209,7 @@
       thy
       |> Sign.add_path bname
       |> PureThy.add_thmss
-        (((Binding.name "simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
+        (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> PureThy.add_thms [((Binding.name "induct", induct), [])];
     val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =