| changeset 26463 | 9283b4185fdf |
| parent 26435 | bdce320cd426 |
| child 26568 | 3a3a83493f00 |
--- a/src/Pure/Isar/object_logic.ML Fri Mar 28 19:43:54 2008 +0100 +++ b/src/Pure/Isar/object_logic.ML Fri Mar 28 20:02:04 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_rulify Drule.norm_hhf_eq); +val _ = Context.>> (Context.map_theory (add_rulify Drule.norm_hhf_eq)); (* atomize *)