# HG changeset patch
# User haftmann
# Date 1261559346 -3600
# Node ID 412cf41a92a0b00c8d672c448bd2896ad80f79cf
# Parent  156a060d5d682044e0c071c1878f4b8e6d9cc3ba
made sml/nj happy

diff -r 156a060d5d68 -r 412cf41a92a0 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Wed Dec 23 08:31:33 2009 +0100
+++ b/src/Tools/Code/code_printer.ML	Wed Dec 23 10:09:06 2009 +0100
@@ -228,8 +228,8 @@
 type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
   -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
 
-val simple_const_syntax =
-  apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars))));
+fun simple_const_syntax syn =
+  apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
 
 fun activate_const_syntax thy literals (n, (cs, f)) naming =
   fold_map (Code_Thingol.ensure_declared_const thy) cs naming