diff -r 61c7875a58b8 -r d6e5fa2ba8b8 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Feb 10 02:22:13 2006 +0100
+++ b/src/Pure/simplifier.ML	Fri Feb 10 02:22:16 2006 +0100
@@ -251,7 +251,7 @@
 in
 
 val simplified =
-  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Thm.rule_attribute (fn x =>
+  Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn x =>
     f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
 
 end;