--- 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;