--- a/src/Pure/Isar/context_rules.ML Thu Mar 27 15:32:12 2008 +0100
+++ b/src/Pure/Isar/context_rules.ML Thu Mar 27 15:32:15 2008 +0100
@@ -198,7 +198,7 @@
val elim_query = rule_add elim_queryK I;
val dest_query = rule_add elim_queryK Tactic.make_elim;
-val _ = Context.add_setup
+val _ = Context.>>
(snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
@@ -215,6 +215,6 @@
("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
"remove declaration of intro/elim/dest rule")];
-val _ = Context.add_setup (Attrib.add_attributes rule_atts);
+val _ = Context.>> (Attrib.add_attributes rule_atts);
end;