diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-11-25 12:59:01 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-25 12:59:01 +0000 |
| commit | 1621428c4ae41134a4d99f931dce341427a9ae4f (patch) | |
| tree | 6cdc88f98530afdba5bdcc38a9e6b84bbfb2faec | |
| parent | 89dcd395161b6126634b68765a7839a4b1fde81e (diff) | |
Fixed show_context
| -rw-r--r-- | isa/ProofGeneral.ML | 4 |
1 files 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 *) |