--- a/src/Pure/Isar/toplevel.ML Tue Aug 08 18:40:56 2006 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Aug 09 00:12:33 2006 +0200
@@ -546,7 +546,8 @@
warning "Cannot skip proof of schematic goal statement"
else ();
if ! skip_proofs andalso not schematic then
- SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int prf)), thy)
+ SkipProof ((History.init (undo_limit int) 0,
+ ProofContext.theory_of (Proof.global_skip_proof int prf)), thy)
else Proof (ProofHistory.init (undo_limit int) prf, thy)
end
| _ => raise UNDEF));