# HG changeset patch
# User wenzelm
# Date 1244129498 -7200
# Node ID 3b32a57b044bd0233142c92e3ddbf18a2bd9368f
# Parent  5a07cc86675d1d7d615ba6473e6fd2f25e282203
added exception_position (dummy);

diff -r 5a07cc86675d -r 3b32a57b044b src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Jun 04 17:31:38 2009 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Thu Jun 04 17:31:38 2009 +0200
@@ -6,12 +6,15 @@
 
 signature ML_COMPILER =
 sig
+  val exception_position: exn -> Position.T
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
 
 structure ML_Compiler: ML_COMPILER =
 struct
 
+fun exception_position _ = Position.none;
+
 fun eval verbose pos toks =
   let
     val line = the_default 1 (Position.line_of pos);