The warning "Rewrite rule from different theory" is ALWAYS printed, even if
tracing is off.

--- a/src/Pure/thm.ML	Wed Aug 19 10:37:07 1998 +0200
+++ b/src/Pure/thm.ML	Wed Aug 19 10:37:56 1998 +0200
@@ -1889,7 +1889,7 @@
             lhs, elhs, fo, perm} =
       let
         val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
-                else (trace_thm true "Rewrite rule from different theory:" thm;
+                else (prthm true "Rewrite rule from different theory:" thm;
                       raise Pattern.MATCH);
         val rprop = if maxt = ~1 then prop
                     else Logic.incr_indexes([],maxt+1) prop;