--- 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 =