src/Pure/goal.ML

--- a/src/Pure/goal.ML	Fri Jan 10 12:30:05 2014 +0100
+++ b/src/Pure/goal.ML	Fri Jan 10 16:20:06 2014 +0100
@@ -215,6 +215,8 @@
         NONE => err "Tactic failed"
       | SOME st =>
           let
+            val _ =
+              Theory.subthy (theory_of_thm st, thy) orelse err "Bad background theory of goal state";
             val res =
               (finish ctxt' st
                 |> Drule.flexflex_unique