| changeset 18988 | d6e5fa2ba8b8 |
| parent 18728 | 6790126ab5f6 |
| child 20872 | 528054ca23e3 |
--- 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;