src/Pure/Isar/context_rules.ML
changeset 26435 bdce320cd426
parent 25979 3297781f8141
child 26463 9283b4185fdf
--- 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;