src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Mar 01 23:35:41 2015 +0100
@@ -892,8 +892,8 @@
 
 fun generic_goal prepp kind before_qed after_qed raw_propp state =
   let
-    val thy = theory_of state;
-    val cert = Thm.cterm_of thy;
+    val ctxt = context_of state;
+    val cert = Proof_Context.cterm_of ctxt;
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();