# HG changeset patch
# User wenzelm
# Date 1206625277 -3600
# Node ID 1afbc0139b1b00aaf4fe77a36823da6b06ac5603
# Parent  5b2beca2087d804031b7792317d6d4ecaf8e17fa
moved old the_context here;
eliminated theory ProtoPure;
renamed ML_Context.the_context to ML_Context.the_global_context;

diff -r 5b2beca2087d -r 1afbc0139b1b src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Thu Mar 27 14:41:14 2008 +0100
+++ b/src/Pure/old_goals.ML	Thu Mar 27 14:41:17 2008 +0100
@@ -11,6 +11,7 @@
 
 signature GOALS =
 sig
+  val the_context: unit -> theory
   val premises: unit -> thm list
   val prove_goal: theory -> string -> (thm list -> tactic list) -> thm
   val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm
@@ -86,6 +87,9 @@
 structure OldGoals: OLD_GOALS =
 struct
 
+val the_context = ML_Context.the_global_context;
+
+
 (*** Goal package ***)
 
 (*Each level of goal stack includes a proof state and alternative states,
@@ -107,11 +111,9 @@
 fun init_mkresult _ = error "No goal has been supplied in subgoal module";
 val curr_mkresult = ref (init_mkresult: bool*thm->thm);
 
-val dummy = Thm.trivial (Thm.read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT));
-
 (*List of previous goal stacks, for the undo operation.  Set by setstate.
   A list of lists!*)
-val undo_list = ref([[(dummy, Seq.empty)]] : gstack list);
+val undo_list = ref([[(asm_rl, Seq.empty)]] : gstack list);
 
 (* Stack of proof attempts *)
 val proofstack = ref([]: proof list);
@@ -119,7 +121,7 @@
 (*reset all refs*)
 fun reset_goals () =
   (curr_prems := []; curr_mkresult := init_mkresult;
-    undo_list := [[(dummy, Seq.empty)]]);
+    undo_list := [[(asm_rl, Seq.empty)]]);
 
 
 (*** Setting up goal-directed proof ***)
@@ -368,7 +370,7 @@
 fun goal thy = goalw thy [];
 
 (*now the versions that wrap the goal up in `Goal' to make it atomic*)
-fun Goalw thms s = agoalw true (ML_Context.the_context ()) thms s;
+fun Goalw thms s = agoalw true (ML_Context.the_global_context ()) thms s;
 val Goal = Goalw [];
 
 (*simple version with minimal amount of checking and postprocessing*)
@@ -514,7 +516,7 @@
 fun no_qed () = ();
 
 (*shorthand for instantiating just one variable in the current theory*)
-fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
+fun inst x t = read_instantiate_sg (ML_Context.the_global_context()) [(x,t)];
 
 end;