| changeset 53171 | a5e54d4d9081 |
| parent 52232 | a2d4ae3e04a2 |
| child 54742 | 7a86358a3c0b |
--- a/src/Pure/Isar/object_logic.ML Fri Aug 23 20:09:34 2013 +0200 +++ b/src/Pure/Isar/object_logic.ML Fri Aug 23 20:35:50 2013 +0200 @@ -174,7 +174,7 @@ val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I); val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I); -val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs)); +val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs); (* atomize *)