From 1621428c4ae41134a4d99f931dce341427a9ae4f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 25 Nov 1998 12:59:01 +0000
Subject: Fixed show_context

---
 isa/ProofGeneral.ML | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 09ecc7ab..2824a2f8 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -19,7 +19,7 @@ signature PROOFGENERAL =
 sig
    val kill_goal : unit -> unit
    val help : unit -> unit
-   val show_context : unit -> unit
+   val show_context : unit -> theory
    val repeat_undo : int -> unit
    val clear_response_buffer : unit -> unit
 
@@ -56,7 +56,7 @@ structure ProofGeneral : PROOFGENERAL =
 
     fun kill_goal () = (Goal "PROP no_goal_supplied"; ())
     fun help () = print version;
-    fun show_context () = (the_context(); ())
+    fun show_context () = the_context();
 
     (* Function used by undo operation *)
     
-- 
cgit v1.2.3