equal
deleted
inserted
replaced
509 (* Too general means, positive equality literal with a variable X as one |
509 (* Too general means, positive equality literal with a variable X as one |
510 operand, when X does not occur properly in the other operand. This rules out |
510 operand, when X does not occur properly in the other operand. This rules out |
511 clearly inconsistent facts such as X = a | X = b, though it by no means |
511 clearly inconsistent facts such as X = a | X = b, though it by no means |
512 guarantees soundness. *) |
512 guarantees soundness. *) |
513 |
513 |
514 fun is_record_type T = not (null (Record.dest_recTs T)) |
|
515 |
|
516 (* Unwanted equalities are those between a (bound or schematic) variable that |
514 (* Unwanted equalities are those between a (bound or schematic) variable that |
517 does not properly occur in the second operand. *) |
515 does not properly occur in the second operand. *) |
518 fun too_general_eqterms (Var z) t = |
516 fun too_general_eqterms (Var z) t = |
519 not (exists_subterm (fn Var z' => z = z' | _ => false) t) |
517 not (exists_subterm (fn Var z' => z = z' | _ => false) t) |
520 | too_general_eqterms (Bound j) t = not (loose_bvar1 (t, j)) |
518 | too_general_eqterms (Bound j) t = not (loose_bvar1 (t, j)) |