diff -r 1ba436add81b -r 3c3defaad8ae src/Pure/Interface/proof_general.ML
--- 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 ();