src/Pure/Isar/proof.ML
changeset 19100 644a7a47ed02
parent 19078 97971a84f0c7
child 19188 a4c82a9ff7d8
equal deleted inserted replaced
19099:100bf66d7e85 19100:644a7a47ed02
   884 fun global_qeds txt =
   884 fun global_qeds txt =
   885   end_proof true txt
   885   end_proof true txt
   886   #> Seq.map generic_qed
   886   #> Seq.map generic_qed
   887   #> Seq.maps (fn (((_, after_qed), results), state) =>
   887   #> Seq.maps (fn (((_, after_qed), results), state) =>
   888     Seq.lift after_qed results (theory_of state)
   888     Seq.lift after_qed results (theory_of state)
   889     |> Seq.map (pair (context_of state)))
   889     |> Seq.map (fn thy => (ProofContext.transfer thy (context_of state), thy)))
   890   |> Seq.DETERM;   (*backtracking may destroy theory!*)
   890   |> Seq.DETERM;   (*backtracking may destroy theory!*)
   891 
   891 
   892 fun global_qed txt =
   892 fun global_qed txt =
   893   global_qeds txt
   893   global_qeds txt
   894   #> check_result "Failed to finish proof"
   894   #> check_result "Failed to finish proof"