declare equal_intr_rule as intro;

--- a/src/Pure/Isar/method.ML	Sat Oct 27 23:19:04 2001 +0200
+++ b/src/Pure/Isar/method.ML	Sat Oct 27 23:19:37 2001 +0200
@@ -705,7 +705,8 @@
 
 val setup =
  [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts,
-  MethodsData.init, add_methods pure_methods];
+  MethodsData.init, add_methods pure_methods,
+  (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_global])])];
 
 
 end;