src/Pure/thm.ML

 fun looptest sign prems lhs rhs =
    rewrite_rule_extra_vars prems lhs rhs
   orelse
    is_Var (head_of lhs)
   orelse
-   (exists (apl (lhs, op Logic.occs)) (rhs :: prems))
+   (exists (apl (lhs, Logic.occs)) (rhs :: prems))
   orelse
    (null prems andalso
     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
 (*the condition "null prems" in the last cases is necessary because
   conditional rewrites with extra variables in the conditions may terminate