--- a/src/Pure/Isar/proof_context.ML Tue Oct 20 21:22:37 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Oct 20 21:26:45 2009 +0200
@@ -142,8 +142,7 @@
structure ProofContext: PROOF_CONTEXT =
struct
-val theory_of = Context.theory_of_proof;
-val init = Context.init_proof;
+open ProofContext;
(** inner syntax mode **)
@@ -259,7 +258,7 @@
else (Consts.merge (local_consts, thy_consts), thy_consts)
end);
-fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
+fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
fun theory f ctxt = transfer (f (theory_of ctxt)) ctxt;