# HG changeset patch
# User wenzelm
# Date 877360098 -7200
# Node ID 78a8e9a1c2f9fe265192a159ab8c4aed15a1ff9c
# Parent  7914990748addf9433eb1dd147427a40dc376d55
make SML/NJ happy;

diff -r 7914990748ad -r 78a8e9a1c2f9 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Oct 20 15:20:42 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Mon Oct 20 17:08:18 1997 +0200
@@ -415,7 +415,7 @@
 
 (* local, global path *)
 
-val empty_decl = empty >> K "";
+fun empty_decl toks = (empty >> K "") toks;
 
 val global_path =
   "|> (fn thy => if ! global_names then thy else Theory.add_path \"/\" thy)";
diff -r 7914990748ad -r 78a8e9a1c2f9 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Oct 20 15:20:42 1997 +0200
+++ b/src/Pure/term.ML	Mon Oct 20 17:08:18 1997 +0200
@@ -50,7 +50,7 @@
   | Var   of indexname * typ
   | Bound of int
   | Abs   of string*typ*term
-  | op $  of term*term;
+  | $     of term*term;
 
 
 (*For errors involving type mismatches*)