--- a/src/Pure/thm.ML Wed Dec 20 20:48:57 2023 +0100
+++ b/src/Pure/thm.ML Wed Dec 20 20:58:56 2023 +0100
@@ -1153,13 +1153,14 @@
let
val (name, oracles') = Name_Space.define (Context.Theory thy1) true (b, ()) (get_oracles thy1);
val thy2 = map_oracles (K oracles') thy1;
+ val cert2 = Context.Certificate_Id (Context.theory_id thy2);
fun invoke_oracle arg =
- let val ct as Cterm {cert = cert2, t = prop, T, maxidx, sorts} = oracle_fn arg in
+ let val ct as Cterm {cert = cert3, t = prop, T, maxidx, sorts} = oracle_fn arg in
if T <> propT then
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else
let
- val cert = Context.join_certificate (Context.Certificate thy2, cert2);
+ val cert = Context.join_certificate (cert2, cert3);
val proofs = Proofterm.get_proofs_level ();
val oracle =
if Proofterm.oracle_enabled proofs
@@ -1173,7 +1174,7 @@
if Proofterm.zproof_enabled proofs then
let
val thy = Context.certificate_theory cert handle ERROR msg =>
- raise CONTEXT (msg, [], [ct], [], SOME (Context.Theory thy2));
+ raise CONTEXT (msg, [], [ct], [], NONE);
in ZTerm.oracle_proof thy name prop end
else ZDummy;
in