--- a/src/Pure/Isar/toplevel.ML Sat Apr 16 15:25:25 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat Apr 16 15:47:52 2011 +0200
@@ -516,7 +516,7 @@
fun theory_to_proof f = begin_proof
(K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
- (K (Context.Theory o Sign.reset_group o ProofContext.theory_of));
+ (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
end;
@@ -660,7 +660,7 @@
else
let
val (body_trs, end_tr) = split_last proof_trs;
- val finish = Context.Theory o ProofContext.theory_of;
+ val finish = Context.Theory o Proof_Context.theory_of;
val future_proof = Proof.global_future_proof
(fn prf =>