src/Pure/old_goals.ML
changeset 26429 1afbc0139b1b
parent 26414 2780de5a1422
child 26626 c6231d64d264
     1.1 --- a/src/Pure/old_goals.ML	Thu Mar 27 14:41:14 2008 +0100
     1.2 +++ b/src/Pure/old_goals.ML	Thu Mar 27 14:41:17 2008 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4  
     1.5  signature GOALS =
     1.6  sig
     1.7 +  val the_context: unit -> theory
     1.8    val premises: unit -> thm list
     1.9    val prove_goal: theory -> string -> (thm list -> tactic list) -> thm
    1.10    val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm
    1.11 @@ -86,6 +87,9 @@
    1.12  structure OldGoals: OLD_GOALS =
    1.13  struct
    1.14  
    1.15 +val the_context = ML_Context.the_global_context;
    1.16 +
    1.17 +
    1.18  (*** Goal package ***)
    1.19  
    1.20  (*Each level of goal stack includes a proof state and alternative states,
    1.21 @@ -107,11 +111,9 @@
    1.22  fun init_mkresult _ = error "No goal has been supplied in subgoal module";
    1.23  val curr_mkresult = ref (init_mkresult: bool*thm->thm);
    1.24  
    1.25 -val dummy = Thm.trivial (Thm.read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT));
    1.26 -
    1.27  (*List of previous goal stacks, for the undo operation.  Set by setstate.
    1.28    A list of lists!*)
    1.29 -val undo_list = ref([[(dummy, Seq.empty)]] : gstack list);
    1.30 +val undo_list = ref([[(asm_rl, Seq.empty)]] : gstack list);
    1.31  
    1.32  (* Stack of proof attempts *)
    1.33  val proofstack = ref([]: proof list);
    1.34 @@ -119,7 +121,7 @@
    1.35  (*reset all refs*)
    1.36  fun reset_goals () =
    1.37    (curr_prems := []; curr_mkresult := init_mkresult;
    1.38 -    undo_list := [[(dummy, Seq.empty)]]);
    1.39 +    undo_list := [[(asm_rl, Seq.empty)]]);
    1.40  
    1.41  
    1.42  (*** Setting up goal-directed proof ***)
    1.43 @@ -368,7 +370,7 @@
    1.44  fun goal thy = goalw thy [];
    1.45  
    1.46  (*now the versions that wrap the goal up in `Goal' to make it atomic*)
    1.47 -fun Goalw thms s = agoalw true (ML_Context.the_context ()) thms s;
    1.48 +fun Goalw thms s = agoalw true (ML_Context.the_global_context ()) thms s;
    1.49  val Goal = Goalw [];
    1.50  
    1.51  (*simple version with minimal amount of checking and postprocessing*)
    1.52 @@ -514,7 +516,7 @@
    1.53  fun no_qed () = ();
    1.54  
    1.55  (*shorthand for instantiating just one variable in the current theory*)
    1.56 -fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
    1.57 +fun inst x t = read_instantiate_sg (ML_Context.the_global_context()) [(x,t)];
    1.58  
    1.59  end;
    1.60