# HG changeset patch
# User berghofe
# Date 982175269 -3600
# Node ID 5254d35e4f7cdd190ef90fac89d59ebc6b5e79a2
# Parent  2d92ab19747b529a6fb0d7cefb0b7481b4e5a923
imp_cong2 -> imp_cong

diff -r 2d92ab19747b -r 5254d35e4f7c src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Feb 14 13:26:46 2001 +0100
+++ b/src/Pure/drule.ML	Wed Feb 14 19:27:49 2001 +0100
@@ -494,7 +494,7 @@
     val AC = read_prop "PROP A ==> PROP C"
     val A = read_prop "PROP A"
   in
-    store_standard_thm "imp_cong2" (implies_intr ABC (equal_intr
+    store_standard_thm "imp_cong" (implies_intr ABC (equal_intr
       (implies_intr AB (implies_intr A
         (equal_elim (implies_elim (assume ABC) (assume A))
           (implies_elim (assume AB) (assume A)))))