# HG changeset patch
# User wenzelm
# Date 1208463745 -7200
# Node ID 1c6181def1d0812eb16a468f33b52923b2f3168c
# Parent  e2dcda7b0401168a4a25daef1ccfed5b5eed99c5
prove_global: Variable.set_body true, pass context;

diff -r e2dcda7b0401 -r 1c6181def1d0 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Apr 17 22:22:23 2008 +0200
+++ b/src/Pure/goal.ML	Thu Apr 17 22:22:25 2008 +0200
@@ -25,7 +25,8 @@
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   val prove: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
-  val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
+  val prove_global: theory -> string list -> term list -> term ->
+    ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val extract: int -> int -> thm -> thm Seq.seq
   val retrofit: int -> int -> thm -> thm -> thm Seq.seq
   val conjunction_tac: int -> tactic
@@ -120,7 +121,8 @@
     val (prems, ctxt') = ctxt
       |> Variable.add_fixes_direct xs
       |> fold Variable.declare_internal (asms @ props)
-      |> Assumption.add_assumes casms;
+      |> Assumption.add_assumes casms
+      ||> Variable.set_body true;
 
     val goal = init (Conjunction.mk_conjunction_balanced cprops);
     val res =
@@ -144,7 +146,7 @@
 fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
 
 fun prove_global thy xs asms prop tac =
-  Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
+  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);