286 val unions_thms = Ord_List.unions thm_ord; |
286 val unions_thms = Ord_List.unions thm_ord; |
287 |
287 |
288 val all_oracles_of = |
288 val all_oracles_of = |
289 let |
289 let |
290 fun collect (PBody {oracles, thms, ...}) = |
290 fun collect (PBody {oracles, thms, ...}) = |
291 tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) => |
291 (if null oracles then I else apfst (cons oracles)) #> |
|
292 (tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) => |
292 if Inttab.defined seen i then (x, seen) |
293 if Inttab.defined seen i then (x, seen) |
293 else |
294 else |
294 let |
295 let val body = Future.join (thm_node_body thm_node) |
295 val body = Future.join (thm_node_body thm_node); |
296 in collect body (x, Inttab.update (i, ()) seen) end)); |
296 val (x', seen') = collect body (x, Inttab.update (i, ()) seen); |
|
297 in (if null oracles then x' else oracles :: x', seen') end); |
|
298 in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end; |
297 in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end; |
299 |
298 |
300 fun approximate_proof_body prf = |
299 fun approximate_proof_body prf = |
301 let |
300 let |
302 val (oracles, thms) = fold_proof_atoms false |
301 val (oracles, thms) = fold_proof_atoms false |