equal
deleted
inserted
replaced
95 |
95 |
96 fun string_of_sequent (gamma, c) = |
96 fun string_of_sequent (gamma, c) = |
97 string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c |
97 string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c |
98 |
98 |
99 val string_of_ref_graph = |
99 val string_of_ref_graph = |
100 sequents_of_ref_graph #> map string_of_sequent #> implode |
100 sequents_of_ref_graph #> map string_of_sequent #> cat_lines |
101 |
101 |
102 fun redirect_sequent tainted bot (gamma, c) = |
102 fun redirect_sequent tainted bot (gamma, c) = |
103 if member atom_eq tainted c then |
103 if member atom_eq tainted c then |
104 gamma |> List.partition (not o member atom_eq tainted) |
104 gamma |> List.partition (not o member atom_eq tainted) |
105 |>> not (atom_eq (c, bot)) ? cons c |
105 |>> not (atom_eq (c, bot)) ? cons c |