| changeset 42360 | da8817d01e7c |
| parent 42358 | b47d41d9f4b5 |
| child 42375 | 774df7c59508 |
--- a/src/Pure/thm.ML Sat Apr 16 15:25:25 2011 +0200 +++ b/src/Pure/thm.ML Sat Apr 16 15:47:52 2011 +0200 @@ -1735,7 +1735,7 @@ ); fun extern_oracles ctxt = - map #1 (Name_Space.extern_table ctxt (Oracles.get (ProofContext.theory_of ctxt))); + map #1 (Name_Space.extern_table ctxt (Oracles.get (Proof_Context.theory_of ctxt))); fun add_oracle (b, oracle) thy = let