--- a/src/Pure/Interface/proof_general.ML Tue Aug 17 17:51:35 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML Tue Aug 17 17:52:04 1999 +0200
@@ -13,8 +13,8 @@
val show_context: unit -> theory
val kill_goal: unit -> unit
val repeat_undo: int -> unit
+ val isa_restart: unit -> unit
val init: bool -> unit
- val isa_restart: unit -> unit
end;
structure ProofGeneral: PROOF_GENERAL =
@@ -156,12 +156,11 @@
val show_context = Context.the_context;
fun kill_goal () =
- (Goal "PROP no_goal_supplied"; writeln ("Proof General, please clear the goals buffer."));
+ (Goals.reset_goals (); writeln ("Proof General, please clear the goals buffer."));
fun repeat_undo 0 = ()
| repeat_undo n = (undo(); repeat_undo (n - 1));
-
fun isa_restart () =
(ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
ThyInfo.touch_all_thys ();