# HG changeset patch # User haftmann # Date 1487443769 -3600 # Node ID 1846c455115382097ab28698dad6a7d264904a46 # Parent 6be69d6881cd829a29f9c68a89acc9342970e61d more complete program generation in presence of dictionaries diff -r 6be69d6881cd -r 1846c4551153 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Fri Feb 17 20:01:17 2017 +0100 +++ b/src/Tools/Code/code_runtime.ML Sat Feb 18 19:49:29 2017 +0100 @@ -494,8 +494,9 @@ computation_cTs named_consts; val program' = Code_Thingol.consts_program ctxt consts'; (*FIXME insufficient interfaces require double invocation of code generator*) + val program'' = Code_Symbol.Graph.merge (K true) (program, program'); val ((ml_modules, compiled_value), deresolve) = - Code_Target.compilation_text' ctxt target some_module_name program' + Code_Target.compilation_text' ctxt target some_module_name program'' (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals; (*FIXME constrain signature*) fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of