# HG changeset patch
# User wenzelm
# Date 918056745 -3600
# Node ID e9dc9ec28a2d8a72313cdee6d5c8907d8defffd8
# Parent  c40e5ac04e3e04c7a75de20cbfa6dfad2019cdb6
added Goal(w) and Export (from context.ML);

diff -r c40e5ac04e3e -r e9dc9ec28a2d src/Pure/goals.ML
--- a/src/Pure/goals.ML	Wed Feb 03 16:42:40 1999 +0100
+++ b/src/Pure/goals.ML	Wed Feb 03 16:45:45 1999 +0100
@@ -14,6 +14,8 @@
   type proof
   val atomic_goal	: theory -> string -> thm list
   val atomic_goalw	: theory -> thm list -> string -> thm list
+  val Goal		: string -> thm list
+  val Goalw		: thm list -> string -> thm list
   val ba		: int -> unit
   val back		: unit -> unit
   val bd		: thm -> int -> unit
@@ -30,6 +32,7 @@
   val choplev		: int -> unit
   val export_thy        : theory -> thm -> thm
   val export            : thm -> thm
+  val Export		: thm -> thm
   val fa		: unit -> unit
   val fd		: thm -> unit
   val fds		: thm list -> unit
@@ -144,8 +147,7 @@
 (** exporting a theorem out of a locale means turning all meta-hyps into assumptions
     and expand and cancel the locale definitions. 
     export goes through all levels in case of nested locales, whereas
-    export_thy just goes one up. (Here the version with theory parameter, the real export
-    resides in Thy/context.ML **)
+    export_thy just goes one up. **)
 
 fun get_top_scope_thms thy = 
    let val sc = (Locale.get_scope_sg (sign_of thy))
@@ -178,6 +180,9 @@
 
 val export = standard o Seq.hd o (REPEAT (FIRSTGOAL (rtac reflexive_thm))) o standard;
 
+fun Export th = export_thy (the_context ()) th;
+
+
 (*Common treatment of "goal" and "prove_goal":
   Return assumptions, initial proof state, and function to make result.
   "atomic" indicates if the goal should be wrapped up in the function
@@ -410,10 +415,13 @@
 val goal = agoal false;
 
 (*now the versions that wrap the goal up in `Goal' to make it atomic*)
-
 val atomic_goalw = agoalw true;
 val atomic_goal = agoal true;
 
+(*implicit context versions*)
+fun Goal s = atomic_goal (Context.the_context ()) s;
+fun Goalw thms s = atomic_goalw (Context.the_context ()) thms s;
+
 
 (*Proof step "by" the given tactic -- apply tactic to the proof state*)
 fun by_com tac ((th,ths), pairs) : gstack =