src/Tools/Code/code_runtime.ML

 
 val generated_computationN = "Generated_Computation";
 
 fun print_computation_code ctxt compiled_value requested_Ts cTs =
   let
-    val typ_sign_for = typ_signatures cTs;
+    val proper_cTs = map_filter I cTs;
+    val typ_sign_for = typ_signatures proper_cTs;
     fun add_typ T Ts =
       if member (op =) Ts T
       then Ts
       else Ts
         |> cons T
         |> fold (fold add_typ o snd) (typ_sign_for T);
     val required_Ts = fold add_typ requested_Ts [];
     val of_term_for_typ' = of_term_for_typ required_Ts;
-    val eval_for_const' = eval_for_const ctxt cTs;
-    val evals = map eval_for_const' cTs;
-    val eval_tuple = enclose "(" ")" (commas evals);
-    val eval_abs = space_implode "" (map (fn s => "fn " ^ s ^ " => ") evals);
+    val eval_for_const' = eval_for_const ctxt proper_cTs;
+    val eval_for_const'' = the_default "_" o Option.map eval_for_const';
+    val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs));
+    fun mk_abs s = "fn " ^ s ^ " => ";
+    val eval_abs = space_implode ""
+      (map (mk_abs o eval_for_const'') cTs);
     val of_term_code = print_of_term_funs {
       typ_sign_for = typ_sign_for,
       eval_for_const = eval_for_const',
       of_term_for_typ = of_term_for_typ' } required_Ts;
   in

     val _ = check t;
   in t end;
 
 fun compile_computation cookie ctxt T program evals vs_ty_evals deps =
   let
+    fun the_const (Const cT) = cT
+      | the_const t = error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t)
     val raw_cTs = case evals of
-        Abs (_, _, t) => (snd o strip_comb) t
+        Abs (_, _, t) => (map the_const o snd o strip_comb) t
       | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals);
-    val cTs = map (fn Const cT => cT
-      | t => error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t)) raw_cTs;
+    val cTs = fold_rev (fn cT => fn cTs =>
+      (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_cTs [];
     fun comp' vs_ty_evals =
       let
         val (generated_code, compiled_value) =
           build_computation_text ctxt NONE program deps vs_ty_evals;
         val (of_term_code, [of_term]) = print_computation_code ctxt compiled_value [T] cTs;

     val compiled_computation =
       Exn.release (run_computation_text cookie ctxt comp' vs_ty_evals []);
   in fn ctxt' =>
     check_typ ctxt' T
     #> reject_vars ctxt'
-    #> check_computation_input ctxt cTs
+    #> check_computation_input ctxt (map_filter I cTs)
     #> compiled_computation
   end;
 
 fun experimental_computation cookie { ctxt, lift_postproc, terms = ts, T } =
   let