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;