src/Pure/Isar/toplevel.ML
changeset 49042 01041f7bf9b4
parent 49012 8686c36fa27d
child 49062 7e31dfd99ce7
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Aug 31 15:25:26 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Aug 31 16:35:30 2012 +0200
     1.3 @@ -425,8 +425,9 @@
     1.4  
     1.5  (* forked proofs *)
     1.6  
     1.7 -val begin_proofs_thy = Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
     1.8 -val begin_proofs = Context.mapping begin_proofs_thy (Local_Theory.raw_theory begin_proofs_thy);
     1.9 +val begin_proofs =
    1.10 +  Context.mapping (Context.theory_map Thm.begin_proofs #> Theory.checkpoint)
    1.11 +    Local_Theory.begin_proofs;
    1.12  
    1.13  fun join_recent_proofs st =
    1.14    (case try proof_of st of