# 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 =>