| changeset 26435 | bdce320cd426 |
| parent 25497 | 1c9b3733f887 |
| child 26463 | 9283b4185fdf |
--- a/src/Pure/Isar/object_logic.ML Thu Mar 27 15:32:12 2008 +0100 +++ b/src/Pure/Isar/object_logic.ML Thu Mar 27 15:32:15 2008 +0100 @@ -193,7 +193,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.add_setup (add_rulify Drule.norm_hhf_eq); +val _ = Context.>> (add_rulify Drule.norm_hhf_eq); (* atomize *)