# HG changeset patch
# User nipkow
# Date 797594471 -7200
# Node ID 88c8df00905bb37b0b1790a8cfd46d4c0d56157e
# Parent  65163737728941cfebe7a6b75bb5281cd3854d87
Added comment to function "loops".

diff -r 651637377289 -r 88c8df00905b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Apr 11 11:20:43 1995 +0200
+++ b/src/Pure/thm.ML	Tue Apr 11 12:01:11 1995 +0200
@@ -1072,6 +1072,11 @@
   orelse
    (null(prems) andalso
     Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));
+(* the condition "null(prems)" in the last case is necessary because
+   conditional rewrites with extra variables in the conditions may terminate
+   although the rhs is an instance of the lhs. Example:
+   ?m < ?n ==> f(?n) == f(?m)
+*)
 
 fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =
   let val prems = Logic.strip_imp_prems prop