src/Tools/Code/code_target.ML

   val check_code: theory -> bool -> string list
     -> ((string * bool) * Token.T list) list -> unit
 
   val generatedN: string
   val evaluator: theory -> string -> Code_Thingol.program
-    -> Code_Symbol.T list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
+    -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
     -> (string * string) list * string
 
   type serializer
   type literals = Code_Printer.literals
   val add_target: string * { serializer: serializer, literals: literals,

       then error (env_var ^ " not set; cannot check code for " ^ target)
       else warning (env_var ^ " not set; skipped checking code for " ^ target)
     else Isabelle_System.with_tmp_dir "Code_Test" ext_check
   end;
 
-fun evaluation mounted_serializer prepared_program syms ((vs, ty), t) =
+fun evaluation mounted_serializer prepared_program syms all_public ((vs, ty), t) =
   let
     val _ = if Code_Thingol.contains_dict_var t then
       error "Term to be evaluated contains free dictionaries" else ();
     val v' = singleton (Name.variant_list (map fst vs)) "a";
     val vs' = (v', []) :: vs;

       |> Code_Symbol.Graph.new_node (Code_Symbol.value,
           Code_Thingol.Fun (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))
       |> fold (curry (perhaps o try o
           Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
     val (program_code, deresolve) =
-      produce (mounted_serializer program [Code_Symbol.value]);
+      produce (mounted_serializer program (if all_public then [] else [Code_Symbol.value]));
     val value_name = the (deresolve Code_Symbol.value);
   in (program_code, value_name) end;
 
 fun evaluator thy target program syms =
   let