--- a/src/HOL/Import/import.ML Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Import/import.ML Sat Apr 16 16:15:37 2011 +0200
@@ -25,11 +25,11 @@
fun import_tac ctxt (thyname, thmname) =
if ! quick_and_dirty
- then Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)
+ then Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)
else
fn th =>
let
- val thy = ProofContext.theory_of ctxt
+ val thy = Proof_Context.theory_of ctxt
val prem = hd (prems_of th)
val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname)
val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem)