# HG changeset patch
# User wenzelm
# Date 957779157 -7200
# Node ID b824c0c55613da8f56c1267f6bcb40b90bd04fc1
# Parent  3e95f3a90875248fac24e4baa87ba8bd5196e83d
tuned msg;

diff -r 3e95f3a90875 -r b824c0c55613 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon May 08 11:45:47 2000 +0200
+++ b/src/Pure/thm.ML	Mon May 08 11:45:57 2000 +0200
@@ -2030,7 +2030,7 @@
             lhs, elhs, fo, perm} =
       let
         val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
-                else (prthm true "Rewrite rule from different theory:" thm;
+                else (prthm true "Ignoring rewrite rule from different theory:" thm;
                       raise Pattern.MATCH);
         val rprop = if maxt = ~1 then prop
                     else Logic.incr_indexes([],maxt+1) prop;