equal
deleted
inserted
replaced
1733 val extend = I; |
1733 val extend = I; |
1734 fun merge data : T = Name_Space.merge_tables data; |
1734 fun merge data : T = Name_Space.merge_tables data; |
1735 ); |
1735 ); |
1736 |
1736 |
1737 fun extern_oracles ctxt = |
1737 fun extern_oracles ctxt = |
1738 map #1 (Name_Space.extern_table ctxt (Oracles.get (ProofContext.theory_of ctxt))); |
1738 map #1 (Name_Space.extern_table ctxt (Oracles.get (Proof_Context.theory_of ctxt))); |
1739 |
1739 |
1740 fun add_oracle (b, oracle) thy = |
1740 fun add_oracle (b, oracle) thy = |
1741 let |
1741 let |
1742 val naming = Sign.naming_of thy; |
1742 val naming = Sign.naming_of thy; |
1743 val (name, tab') = Name_Space.define true naming (b, ()) (Oracles.get thy); |
1743 val (name, tab') = Name_Space.define true naming (b, ()) (Oracles.get thy); |