# HG changeset patch
# User wenzelm
# Date 1449759208 -3600
# Node ID 69b035408b186159b0bbbd1da641728d0e9a08f2
# Parent  dcbe9f756ae0ca7c89a63040d9126a20d5439424
make SML/NJ happy;

diff -r dcbe9f756ae0 -r 69b035408b18 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Dec 10 13:38:40 2015 +0000
+++ b/src/Pure/Isar/token.ML	Thu Dec 10 15:53:28 2015 +0100
@@ -477,7 +477,7 @@
 
 (* src *)
 
-fun dest_src [] = raise Fail "Empty token source"
+fun dest_src ([]: src) = raise Fail "Empty token source"
   | dest_src (head :: args) = (head, args);
 
 fun name_of_src src =