# HG changeset patch # User boehmes # Date 1294071032 -3600 # Node ID 44511bf5dcc61edc719b9338b1a5884bdd8a0d1b # Parent 5fbad03906491015dde40c83f3b441629372bc6d# Parent 9acb7c5015307f7d4fcc3b108e1fc65933bf968c merged diff -r 5fbad0390649 -r 44511bf5dcc6 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Mon Jan 03 16:49:28 2011 +0100 +++ b/src/Pure/Isar/element.ML Mon Jan 03 17:10:32 2011 +0100 @@ -289,6 +289,7 @@ Proof.map_context (K goal_ctxt) #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i cmd NONE after_qed' (map (pair Thm.empty_binding) propss); + in fun witness_proof after_qed wit_propss = @@ -303,6 +304,7 @@ fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int = gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props; + end;