1.1 --- a/src/Pure/Isar/context_rules.ML	Fri Mar 28 19:43:54 2008 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Mar 28 20:02:04 2008 +0100
     1.3 @@ -198,8 +198,8 @@
     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.>>
     1.8 -  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
     1.9 +val _ = Context.>> (Context.map_theory
    1.10 +  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]));
    1.11  
    1.12  
    1.13  (* concrete syntax *)
    1.14 @@ -215,6 +215,6 @@
    1.15    ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
    1.16      "remove declaration of intro/elim/dest rule")];
    1.17  
    1.18 -val _ = Context.>> (Attrib.add_attributes rule_atts);
    1.19 +val _ = Context.>> (Context.map_theory (Attrib.add_attributes rule_atts));
    1.20  
    1.21  end;