--- a/src/Pure/goal.ML Fri Nov 24 17:23:15 2006 +0100
+++ b/src/Pure/goal.ML Fri Nov 24 22:05:12 2006 +0100
@@ -106,7 +106,7 @@
fun prove_multi ctxt xs asms props tac =
let
- val thy = Context.theory_of_proof ctxt;
+ val thy = ProofContext.theory_of ctxt;
val string_of_term = Sign.string_of_term thy;
fun err msg = cat_error msg
@@ -145,7 +145,7 @@
fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
fun prove_global thy xs asms prop tac =
- Drule.standard (prove (Context.init_proof thy) xs asms prop (fn {prems, ...} => tac prems));
+ Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));