--- 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;