changeset 61853 | fb7756087101 |
parent 61841 | 4d3527b94f2a |
child 62913 | 13252110a6fe |
--- 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)));