extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
authorwenzelm
Wed Mar 27 20:57:05 2013 +0100 (2013-03-27 ago)
changeset 515605b4ae2467830
parent 51559 320907e48a9e
child 51561 a1eb68bd9312
child 51562 5fffa75d2432
extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 27 19:32:44 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 27 20:57:05 2013 +0100
     1.3 @@ -548,7 +548,7 @@
     1.4  
     1.5  fun theory_to_proof f = begin_proof
     1.6    (fn _ => fn gthy =>
     1.7 -    (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
     1.8 +    (Context.Theory o Theory.checkpoint o Sign.reset_group o Proof_Context.theory_of,
     1.9        (case gthy of
    1.10          Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))
    1.11        | _ => raise UNDEF)));