# HG changeset patch
# User wenzelm
# Date 1004217577 -7200
# Node ID 2ee7c72cc4648dd60cce2a2dd0321baac2dc7b2c
# Parent  e7eedbd2c8caa2dc2d388763ec24c58c62468bb9
declare equal_intr_rule as intro;

diff -r e7eedbd2c8ca -r 2ee7c72cc464 src/Pure/Isar/method.ML
--- 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;