# HG changeset patch
# User wenzelm
# Date 954095903 -7200
# Node ID e451c486554892aceafaa7abf14dc93ab3f9b22d
# Parent  8a3ae21e4a5ba8da2c7db2814152f309b9592b15
made SML/NJ happy;

diff -r 8a3ae21e4a5b -r e451c4865548 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sun Mar 26 20:17:52 2000 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Sun Mar 26 20:38:23 2000 +0200
@@ -96,8 +96,8 @@
       | err (toks, Some msg) = kind ^ get_pos toks ^ ": " ^ msg;
   in Scan.!! err scan end;
 
-val !!! = cut "Outer syntax error";
-val !!!! = cut "Corrupted outer syntax in presentation";
+fun !!! scan = cut "Outer syntax error" scan;
+fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;