changeset 44270 | 3eaad39e520c |
parent 38874 | 4a4d34d2f97b |
child 50914 | fe4714886d92 |
--- a/src/Pure/ML/ml_compiler.ML Thu Aug 18 17:30:47 2011 +0200 +++ b/src/Pure/ML/ml_compiler.ML Thu Aug 18 17:53:32 2011 +0200 @@ -7,7 +7,7 @@ signature ML_COMPILER = sig val exn_position: exn -> Position.T - val exn_messages: exn -> string list + val exn_messages: exn -> (serial * string) list val exn_message: exn -> string val eval: bool -> Position.T -> ML_Lex.token list -> unit end