# Re: [isabelle] thm dependencies

Thanks, Makarius. Here is the SML code I wrote to extract the list of external oracle tags used in the proof of a theorem. Am I using any deprecated functions?
```
text {* Extract the abstract syntax of a theorem's oracle tags. *}

ML {*
fun oracle_terms_of_thm thm
= Proofterm.oracles_of_proof [] (proof_of thm)
*}

```
text {* This will let us view the tagged oracles using surface syntax. *}
```
ML {*
fun oracle_strings_of_thm thm
= let val thy = theory_of_thm thm
```
in map (fn (oracle,formula) => (oracle, Sign.string_of_term thy formula))
```         (oracles_of_thm thm)
end
*}

-john

On Oct 25, 2005, at 7:19 AM, Makarius wrote:

```
```On Tue, 25 Oct 2005, John Matthews wrote:

```
```Similarly, how to I extract the list of external oracles used in the
proof of a tagged theorem, when theorem dependencies are turned off?
```
```
```
See Pure/proofterm.ML for some operations on proof terms as stored within
```the "der" field of a thm.

```
```On Oct 24, 2005, at 5:52 PM, Sean McLaughlin wrote:
```
```
```
```  I'd like a way to extract the theorem dependencies of a theorem. I
know Isabelle has a great facility for plotting these deps with
"thm_deps", but is there a way to just extract a tree of dependencies
(that could be topologically sorted, say).
```
```
See Pure/Thy/thm_deps.ML.  You may build a Graph.T (cf.
```
Pure/General/graph.ML) and get a toplogically sorted list of entries like
```this:

fn G => Graph.all_succs G (Graph.minimals G)

Makarius
```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.