src/Pure/thm.ML

 
 
 
 (*** Oracles ***)
 
-fun add_oracle (b, oracle_fn) thy =
-  let
-    val (name, oracles') = Name_Space.define (Context.Theory thy) true (b, ()) (get_oracles thy);
-    val thy' = map_oracles (K oracles') thy;
+fun add_oracle (b, oracle_fn) thy1 =
+  let
+    val (name, oracles') = Name_Space.define (Context.Theory thy1) true (b, ()) (get_oracles thy1);
+    val thy2 = map_oracles (K oracles') thy1;
     fun invoke_oracle arg =
       let val ct as Cterm {cert = cert2, 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 thy', cert2);
+            val cert = Context.join_certificate (Context.Certificate thy2, cert2);
             val proofs = Proofterm.get_proofs_level ();
             val oracle =
               if Proofterm.oracle_enabled proofs
               then ((name, Position.thread_data ()), SOME prop)
               else ((name, Position.none), NONE);

               then Proofterm.oracle_proof name prop
               else MinProof;
             val zproof =
               if Proofterm.zproof_enabled proofs then
                 let
-                  val thy'' = Context.certificate_theory cert handle ERROR msg =>
-                    raise CONTEXT (msg, [], [ct], [], SOME (Context.Theory thy'));
-                in ZTerm.oracle_proof thy'' name prop end
+                  val thy = Context.certificate_theory cert handle ERROR msg =>
+                    raise CONTEXT (msg, [], [ct], [], SOME (Context.Theory thy2));
+                in ZTerm.oracle_proof thy name prop end
               else ZDummy;
           in
             Thm (make_deriv [] [oracle] [] [] zproof proof,
              {cert = cert,
               tags = [],

               hyps = [],
               tpairs = [],
               prop = prop})
           end
       end;
-  in ((name, invoke_oracle), thy') end;
+  in ((name, invoke_oracle), thy2) end;
 
 val oracle_space = Name_Space.space_of_table o get_oracles;
 
 fun pretty_oracle ctxt =
   Name_Space.pretty ctxt (oracle_space (Proof_Context.theory_of ctxt));