src/Pure/Isar/context_rules.ML
changeset 26435 bdce320cd426
parent 25979 3297781f8141
child 26463 9283b4185fdf
     1.1 --- a/src/Pure/Isar/context_rules.ML	Thu Mar 27 15:32:12 2008 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Mar 27 15:32:15 2008 +0100
     1.3 @@ -198,7 +198,7 @@
     1.4  val elim_query  = rule_add elim_queryK I;
     1.5  val dest_query  = rule_add elim_queryK Tactic.make_elim;
     1.6  
     1.7 -val _ = Context.add_setup
     1.8 +val _ = Context.>>
     1.9    (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
    1.10  
    1.11  
    1.12 @@ -215,6 +215,6 @@
    1.13    ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
    1.14      "remove declaration of intro/elim/dest rule")];
    1.15  
    1.16 -val _ = Context.add_setup (Attrib.add_attributes rule_atts);
    1.17 +val _ = Context.>> (Attrib.add_attributes rule_atts);
    1.18  
    1.19  end;