equal
deleted
inserted
replaced
410 fun reorient sign prems lhs rhs = |
410 fun reorient sign prems lhs rhs = |
411 rewrite_rule_extra_vars prems lhs rhs |
411 rewrite_rule_extra_vars prems lhs rhs |
412 orelse |
412 orelse |
413 is_Var (head_of lhs) |
413 is_Var (head_of lhs) |
414 orelse |
414 orelse |
|
415 (* turns t = x around, which causes a headache if x is a local variable - |
|
416 usually it is very useful :-( |
|
417 is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs)) |
|
418 andalso not(exists_subterm is_Var lhs) |
|
419 orelse |
|
420 *) |
415 exists (apl (lhs, Logic.occs)) (rhs :: prems) |
421 exists (apl (lhs, Logic.occs)) (rhs :: prems) |
416 orelse |
422 orelse |
417 null prems andalso Pattern.matches (Sign.tsig_of sign) (lhs, rhs) |
423 null prems andalso Pattern.matches (Sign.tsig_of sign) (lhs, rhs) |
418 (*the condition "null prems" is necessary because conditional rewrites |
424 (*the condition "null prems" is necessary because conditional rewrites |
419 with extra variables in the conditions may terminate although |
425 with extra variables in the conditions may terminate although |