# HG changeset patch
# User clasohm
# Date 773053831 -7200
# Node ID 3ee5c9314efe91e32fadd9865bfd167d5fc76c52
# Parent  7b6d8b8d45805b4807690c6a6adbac578e02f656
rewritec now uses trace_thm for it's "rewrite rule from different theory"
message

diff -r 7b6d8b8d4580 -r 3ee5c9314efe src/Pure/thm.ML
--- 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;