# HG changeset patch
# User wenzelm
# Date 1389367206 -3600
# Node ID a128df2f670e4cc5f8219d31bfcd42035cc87f7d
# Parent  2a010ef82fd74dfb0ba86b2f655ebd43618b5745
explicit check of background theory;

diff -r 2a010ef82fd7 -r a128df2f670e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Jan 10 12:30:05 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Jan 10 16:20:06 2014 +0100
@@ -481,6 +481,8 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
+    val _ =
+      Theory.subthy (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);
diff -r 2a010ef82fd7 -r a128df2f670e 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