# HG changeset patch
# User nipkow
# Date 853953456 -3600
# Node ID 907a3379f165d4bcd95155f92dd9c5d2df485706
# Parent  7a876fc091d67ff6804eefc1ac7a564cac631535
Added warning msg when the simplifier cannot use a premise as a rewrite rule
because it contains (type) unknowns.

diff -r 7a876fc091d6 -r 907a3379f165 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jan 21 11:29:28 1997 +0100
+++ b/src/Pure/thm.ML	Wed Jan 22 18:17:36 1997 +0100
@@ -1845,7 +1845,10 @@
                         else (shyps,hyps,0,s,ders);
            val maxidx1 = maxidx_of_term s1
            val mss1 =
-             if not useprem orelse maxidx1 <> ~1 then mss
+             if not useprem then mss else
+             if maxidx1 <> ~1 then (prtm_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, 
                                               T=propT, maxidx=maxidx1})
                   in add_simps(add_prems(mss,[thm]), mk_rews thm) end