# HG changeset patch
# User nipkow
# Date 855919182 -3600
# Node ID 54f21bf9522ab9eefea4e53d7974a382c86fbead
# Parent  3fd774ee405a3f00cc6123a5a51c5602dd67d82c
Made troublesome simplifier warning dependent on trace_simp.

diff -r 3fd774ee405a -r 54f21bf9522a src/Pure/thm.ML
--- 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,