# HG changeset patch # User wenzelm # Date 1369817262 -7200 # Node ID b3a5c6f2cb671f598bc207ec7dc20f19b18a9a2a # Parent 689062704416e5f856150d4cab38beae2bed6b92 make SML/NJ happy; diff -r 689062704416 -r b3a5c6f2cb67 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Wed May 29 03:10:26 2013 +0200 +++ b/src/Tools/Code/code_target.ML Wed May 29 10:47:42 2013 +0200 @@ -613,13 +613,13 @@ (* custom symbol names *) -val arrange_name_decls = +fun arrange_name_decls x = let fun arrange is_module (sym, target_names) = map (fn (target, some_name) => (target, (sym, Option.map (check_name is_module) some_name))) target_names; in Code_Symbol.maps_attr' (arrange false) (arrange false) (arrange false) - (arrange false) (arrange false) (arrange true) + (arrange false) (arrange false) (arrange true) x end; fun cert_name_decls thy = cert_syms thy #> arrange_name_decls;