# HG changeset patch
# User wenzelm
# Date 1126952288 -7200
# Node ID 178344c7456215739d3a007e9397c8703f3c80ad
# Parent  cfa8b1ebfc9a0afc968a63b9bdaf7d80d1c6854c
theory_to_proof: check theory of initial proof state, which must not be changed;

diff -r cfa8b1ebfc9a -r 178344c74562 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Sep 17 12:18:07 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Sep 17 12:18:08 2005 +0200
@@ -437,9 +437,13 @@
 
 fun theory_to_proof f = app_current (fn int =>
   (fn Theory (thy, _) =>
-        if ! skip_proofs then SkipProof (History.init (undo_limit int) 0,
-          #1 (Proof.global_skip_proof int (f thy)))
-        else Proof (ProofHistory.init (undo_limit int) (f thy))
+      let val st = f thy in
+        if Theory.eq_thy (thy, Proof.theory_of st) then ()
+        else error "Theory changed at start of proof";
+        if ! skip_proofs then
+          SkipProof (History.init (undo_limit int) 0, #1 (Proof.global_skip_proof int st))
+        else Proof (ProofHistory.init (undo_limit int) st)
+      end
     | _ => raise UNDEF));
 
 fun proof' f = map_current (fn int =>