rewritec now uses trace_thm for it's "rewrite rule from different theory"
message

--- a/src/Pure/thm.ML	Fri Jul 01 11:04:12 1994 +0200
+++ b/src/Pure/thm.ML	Fri Jul 01 11:10:31 1994 +0200
@@ -1211,7 +1211,8 @@
   let val t = Pattern.eta_contract t;
       fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs, perm} =
         let val unit = if Sign.subsig(sign,signt) then ()
-                  else (writeln"Warning: rewrite rule from different theory";
+                  else (trace_thm"Warning: rewrite rule from different theory"
+                          thm;
                         raise Pattern.MATCH)
             val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,t)
             val prop' = subst_vars insts prop;