src/Pure/simplifier.ML

--- a/src/Pure/simplifier.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/simplifier.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -309,7 +309,7 @@
 in
 
 val simplified = conv_mode -- Attrib.thms >>
-  (fn (f, ths) => Thm.rule_attribute (fn context =>
+  (fn (f, ths) => Thm.rule_attribute ths (fn context =>
     f ((if null ths then I else Raw_Simplifier.clear_simpset)
         (Context.proof_of context) addsimps ths)));