src/Pure/Isar/element.ML
changeset 45329 dd8208a3655a
parent 45295 255200892a42
child 45345 2cb00d068e3b
equal deleted inserted replaced
45328:e5b33eecbf6e 45329:dd8208a3655a
   292       let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
   292       let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
   293       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   293       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   294   in proof after_qed' propss #> refine_witness #> Seq.hd end;
   294   in proof after_qed' propss #> refine_witness #> Seq.hd end;
   295 
   295 
   296 fun proof_local cmd goal_ctxt int after_qed' propss =
   296 fun proof_local cmd goal_ctxt int after_qed' propss =
   297     Proof.map_context (K goal_ctxt)
   297   Proof.map_context (K goal_ctxt) #>
   298     #> Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
   298   Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
   299       cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
   299     cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
   300 
   300 
   301 in
   301 in
   302 
   302 
   303 fun witness_proof after_qed wit_propss =
   303 fun witness_proof after_qed wit_propss =
   304   gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)
   304   gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)