src/Pure/thm.ML
changeset 4684 eb712fef644b
parent 4679 24917efb31b5
child 4713 bea2ab2e360b
equal deleted inserted replaced
4683:de426efe87d3 4684:eb712fef644b
  1601 fun looptest sign prems lhs rhs =
  1601 fun looptest sign prems lhs rhs =
  1602    rewrite_rule_extra_vars prems lhs rhs
  1602    rewrite_rule_extra_vars prems lhs rhs
  1603   orelse
  1603   orelse
  1604    is_Var (head_of lhs)
  1604    is_Var (head_of lhs)
  1605   orelse
  1605   orelse
  1606    (exists (apl (lhs, op Logic.occs)) (rhs :: prems))
  1606    (exists (apl (lhs, Logic.occs)) (rhs :: prems))
  1607   orelse
  1607   orelse
  1608    (null prems andalso
  1608    (null prems andalso
  1609     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
  1609     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
  1610 (*the condition "null prems" in the last cases is necessary because
  1610 (*the condition "null prems" in the last cases is necessary because
  1611   conditional rewrites with extra variables in the conditions may terminate
  1611   conditional rewrites with extra variables in the conditions may terminate