Added comment to function "loops".
--- 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