# HG changeset patch
# User wenzelm
# Date 1212097603 -7200
# Node ID 4593b9f4ba429ec326197e60072c82a7ad085822
# Parent  b5b8afc9fdcda1135edba99729adecbd592be91d
proper context for attribute simplified;

diff -r b5b8afc9fdcd -r 4593b9f4ba42 src/Pure/simplifier.ML
--- 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;