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