--- a/src/Pure/Isar/proof.ML Tue Dec 05 22:14:50 2006 +0100
+++ b/src/Pure/Isar/proof.ML Tue Dec 05 22:14:51 2006 +0100
@@ -772,7 +772,7 @@
fn results => map_context after_ctxt #> after_local results);
in
goal_state
- |> map_context (Variable.set_body true)
+ |> map_context (Variable.set_body true #> ProofContext.set_stmt true)
|> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
|> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
|> map_context (ProofContext.auto_bind_goal props)