# HG changeset patch
# User wenzelm
# Date 1438963092 -7200
# Node ID 4194901fd513d82252e268febe4e1fa249e9f1d3
# Parent  20cfa048fe7c1f001e54f6f5ec629020d1a508c1
make SML/NJ work;

diff -r 20cfa048fe7c -r 4194901fd513 src/Pure/ML/exn_properties_dummy.ML
--- a/src/Pure/ML/exn_properties_dummy.ML	Fri Aug 07 16:15:53 2015 +0200
+++ b/src/Pure/ML/exn_properties_dummy.ML	Fri Aug 07 17:58:12 2015 +0200
@@ -6,6 +6,7 @@
 
 signature EXN_PROPERTIES =
 sig
+  val position_of: 'location -> Position.T
   val get: exn -> Properties.T
   val update: Properties.entry list -> exn -> exn
 end;
@@ -13,6 +14,8 @@
 structure Exn_Properties: EXN_PROPERTIES =
 struct
 
+fun position_of _ = Position.none;
+
 fun get _ = [];
 fun update _ exn = exn;