362 fun eq_types t = t aconv HOLogic.true_const; |
362 fun eq_types t = t aconv HOLogic.true_const; |
363 |
363 |
364 fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; |
364 fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; |
365 |
365 |
366 fun replace_deps (old:int, new) (lno, t, deps) = |
366 fun replace_deps (old:int, new) (lno, t, deps) = |
367 (lno, t, List.foldl (gen_union (op =)) [] (map (replace_dep (old, new)) deps)); |
367 (lno, t, List.foldl (union (op =)) [] (map (replace_dep (old, new)) deps)); |
368 |
368 |
369 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ |
369 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ |
370 only in type information.*) |
370 only in type information.*) |
371 fun add_prfline ((lno, "axiom", t, []), lines) = (*axioms are not proof lines*) |
371 fun add_prfline ((lno, "axiom", t, []), lines) = (*axioms are not proof lines*) |
372 if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*) |
372 if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*) |