# HG changeset patch
# User paulson
# Date 877079454 -7200
# Node ID be9ae8de1615e16a4ad6cb62f225ea59c15cf2b8
# Parent  0eb9b9dd4de6c4672960c2b2b4b8588fc85e0672
Eta-expanded a function decl to make sml/nj happy

diff -r 0eb9b9dd4de6 -r be9ae8de1615 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Oct 17 11:10:13 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Fri Oct 17 11:10:54 1997 +0200
@@ -415,7 +415,7 @@
 
 (* global *)
 
-val global_decl = empty >> K "\"/\"";
+fun global_decl x = (empty >> K "\"/\"") x;