# HG changeset patch # User wenzelm # Date 1364414225 -3600 # Node ID 5b4ae246783038128c24651f22a5dbca82ca5033 # Parent 320907e48a9e29ff4fe858ea9d72abe024b9250a extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof; diff -r 320907e48a9e -r 5b4ae2467830 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Mar 27 19:32:44 2013 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Mar 27 20:57:05 2013 +0100 @@ -548,7 +548,7 @@ fun theory_to_proof f = begin_proof (fn _ => fn gthy => - (Context.Theory o Sign.reset_group o Proof_Context.theory_of, + (Context.Theory o Theory.checkpoint o Sign.reset_group o Proof_Context.theory_of, (case gthy of Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF)));