31 in collect body (res, Inttab.update (i, ()) seen) end)); |
31 in collect body (res, Inttab.update (i, ()) seen) end)); |
32 val bodies = map Thm.proof_body_of thms; |
32 val bodies = map Thm.proof_body_of thms; |
33 in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end; |
33 in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end; |
34 |
34 |
35 fun has_skip_proof thms = |
35 fun has_skip_proof thms = |
36 all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\<open>skip_proof\<close>); |
36 all_oracles thms |> exists (fn ((name, _), _) => name = \<^oracle_name>\<open>skip_proof\<close>); |
37 |
37 |
38 fun pretty_thm_oracles ctxt thms = |
38 fun pretty_thm_oracles ctxt thms = |
39 let |
39 let |
40 val thy = Proof_Context.theory_of ctxt; |
40 val thy = Proof_Context.theory_of ctxt; |
41 fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name] |
41 fun prt_ora (name, pos) = Thm.pretty_oracle ctxt name :: Pretty.here pos; |
42 | prt_oracle (name, SOME prop) = |
42 fun prt_oracle (ora, NONE) = prt_ora ora |
43 [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, |
43 | prt_oracle (ora, SOME prop) = |
44 Syntax.pretty_term_global thy prop]; |
44 prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop]; |
45 in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end; |
45 in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end; |
46 |
46 |
47 |
47 |
48 (* thm_deps *) |
48 (* thm_deps *) |
49 |
49 |