equal
deleted
inserted
replaced
401 (* FIXME: it seems that the conditions on extra variables are too liberal if |
401 (* FIXME: it seems that the conditions on extra variables are too liberal if |
402 prems are nonempty: does solving the prems really guarantee instantiation of |
402 prems are nonempty: does solving the prems really guarantee instantiation of |
403 all its Vars? Better: a dynamic check each time a rule is applied. |
403 all its Vars? Better: a dynamic check each time a rule is applied. |
404 *) |
404 *) |
405 fun rewrite_rule_extra_vars prems elhs erhs = |
405 fun rewrite_rule_extra_vars prems elhs erhs = |
406 not (term_varnames erhs subset Library.foldl add_term_varnames (term_varnames elhs, prems)) |
406 not (term_varnames erhs subset fold add_term_varnames prems (term_varnames elhs)) |
407 orelse |
407 orelse |
408 not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems))); |
408 not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems))); |
409 |
409 |
410 (*simple test for looping rewrite rules and stupid orientations*) |
410 (*simple test for looping rewrite rules and stupid orientations*) |
411 fun reorient thy prems lhs rhs = |
411 fun reorient thy prems lhs rhs = |