src/Tools/Code/code_target.ML
changeset 52161 51eca565b153
parent 52138 e21426f244aa
child 52218 b3a5c6f2cb67
equal deleted inserted replaced
52160:7746c9f1baf3 52161:51eca565b153
   417     val vs' = (v', []) :: vs;
   417     val vs' = (v', []) :: vs;
   418     val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
   418     val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
   419     val value_name = "Value.value.value"
   419     val value_name = "Value.value.value"
   420     val program = prepared_program
   420     val program = prepared_program
   421       |> Graph.new_node (value_name,
   421       |> Graph.new_node (value_name,
   422           Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
   422           Code_Thingol.Fun (@{const_name dummy_pattern}, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
   423       |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
   423       |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
   424     val (program_code, deresolve) = produce (mounted_serializer program);
   424     val (program_code, deresolve) = produce (mounted_serializer program);
   425     val value_name' = the (deresolve value_name);
   425     val value_name' = the (deresolve value_name);
   426   in (program_code, value_name') end;
   426   in (program_code, value_name') end;
   427 
   427