--- 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;