# HG changeset patch
# User wenzelm
# Date 1165353291 -3600
# Node ID d5eb0720e45d34d804755f60792e05af58efe0a1
# Parent  ba07e24dc941bb612e5e38f1dfd77b32321d5513
generic_goal: enable stmt mode;

diff -r ba07e24dc941 -r d5eb0720e45d src/Pure/Isar/proof.ML
--- 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)