# HG changeset patch # User wenzelm # Date 911383013 -3600 # Node ID 85d62ecb950d763ad986902fe78bde879be0ef33 # Parent 50005d6ba6093af32656f1aa9b07df16185d3358 export exn_message; diff -r 50005d6ba609 -r 85d62ecb950d src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Nov 18 10:56:38 1998 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Nov 18 10:56:53 1998 +0100 @@ -50,6 +50,7 @@ val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition type isar val trace: bool ref + val exn_message: exn -> string val apply: bool -> transition -> state -> (state * (exn * string) option) option val excursion: transition list -> unit val set_state: state -> unit