--- a/src/Pure/Isar/context_rules.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/context_rules.ML Fri Mar 28 20:02:04 2008 +0100
@@ -198,8 +198,8 @@
val elim_query = rule_add elim_queryK I;
val dest_query = rule_add elim_queryK Tactic.make_elim;
-val _ = Context.>>
- (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
+val _ = Context.>> (Context.map_theory
+ (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]));
(* concrete syntax *)
@@ -215,6 +215,6 @@
("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
"remove declaration of intro/elim/dest rule")];
-val _ = Context.>> (Attrib.add_attributes rule_atts);
+val _ = Context.>> (Context.map_theory (Attrib.add_attributes rule_atts));
end;