src/Pure/Isar/context_rules.ML

   val delrules_global: theory * thm list -> theory
   val addXIs_local: ProofContext.context * thm list -> ProofContext.context
   val addXEs_local: ProofContext.context * thm list -> ProofContext.context
   val addXDs_local: ProofContext.context * thm list -> ProofContext.context
   val delrules_local: ProofContext.context * thm list -> ProofContext.context
-  val setup: (theory -> theory) list
 end;
 
 structure ContextRules: CONTEXT_RULES =
 struct
 

 
   val print = print_rules Display.pretty_thm_sg;
 end;
 
 structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
+val _ = Context.add_setup [GlobalRules.init];
 val print_global_rules = GlobalRules.print;
 
 structure LocalRulesArgs =
 struct
   val name = GlobalRulesArgs.name;

   val init = GlobalRules.get;
   val print = print_rules ProofContext.pretty_thm;
 end;
 
 structure LocalRules = ProofDataFun(LocalRulesArgs);
+val _ = Context.add_setup [LocalRules.init];
 val print_local_rules = LocalRules.print;
 
 
 (* access data *)
 

 val dest_query_local   = add elim_queryK Tactic.make_elim LocalRules.map;
 val rule_del_local     = del LocalRules.map;
 
 end;
 
+val _ = Context.add_setup
+  [#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
+
 
 (* low-level modifiers *)
 
 fun modifier att (x, ths) =
   #1 (Thm.applys_attributes ((x, rev ths), [att]));

 val addXEs_local = modifier (elim_query_local NONE);
 val addXDs_local = modifier (dest_query_local NONE);
 val delrules_local = modifier rule_del_local;
 
 
-
-(** theory setup **)
-
-val setup =
- [GlobalRules.init, LocalRules.init];
-
-
-end;
+end;