--- a/src/Pure/simplifier.ML Thu May 29 23:46:41 2008 +0200
+++ b/src/Pure/simplifier.ML Thu May 29 23:46:43 2008 +0200
@@ -334,8 +334,9 @@
in
val simplified =
- 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))));
+ Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context =>
+ f ((if null ths then I else MetaSimplifier.clear_ss)
+ (local_simpset_of (Context.proof_of context)) addsimps ths))));
end;