Made troublesome simplifier warning dependent on trace_simp.

--- a/src/Pure/thm.ML	Fri Feb 14 11:40:53 1997 +0100
+++ b/src/Pure/thm.ML	Fri Feb 14 12:19:42 1997 +0100
@@ -1846,7 +1846,7 @@
            val maxidx1 = maxidx_of_term s1
            val mss1 =
              if not useprem then mss else
-             if maxidx1 <> ~1 then (prtm_warning
+             if maxidx1 <> ~1 then (trace_term_warning
 "Cannot add premise as rewrite rule because it contains (type) unknowns:"
                                                   sign s1; mss)
              else let val thm = assume (Cterm{sign=sign, t=s1,