--- a/src/Pure/Isar/proof.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/Pure/Isar/proof.ML Wed Mar 04 19:53:18 2015 +0100
@@ -474,7 +474,8 @@
val thy = Proof_Context.theory_of ctxt;
val _ =
- Theory.subthy (theory_of_thm goal, thy) orelse error "Bad background theory of goal state";
+ Theory.subthy (Thm.theory_of_thm goal, thy) orelse
+ error "Bad background theory of goal state";
val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);