diff -r f2215ed00438 -r d2f5ca3c048d src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Thu Apr 21 22:00:28 2005 +0200
+++ b/src/Pure/Isar/context_rules.ML	Thu Apr 21 22:02:06 2005 +0200
@@ -49,7 +49,6 @@
   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 =
@@ -145,6 +144,7 @@
 end;
 
 structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
+val _ = Context.add_setup [GlobalRules.init];
 val print_global_rules = GlobalRules.print;
 
 structure LocalRulesArgs =
@@ -156,6 +156,7 @@
 end;
 
 structure LocalRules = ProofDataFun(LocalRulesArgs);
+val _ = Context.add_setup [LocalRules.init];
 val print_local_rules = LocalRules.print;
 
 
@@ -248,6 +249,9 @@
 
 end;
 
+val _ = Context.add_setup
+  [#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
+
 
 (* low-level modifiers *)
 
@@ -265,11 +269,4 @@
 val delrules_local = modifier rule_del_local;
 
 
-
-(** theory setup **)
-
-val setup =
- [GlobalRules.init, LocalRules.init];
-
-
 end;