src/Tools/Code/code_runtime.ML

 sig
   val target: string
   val value: string option
     -> (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
     -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
+  val code_reflect: (string * string list) list -> string list -> string -> string option
+    -> theory -> theory
   val setup: theory -> theory
 end;
 
 structure Code_Runtime : CODE_RUNTIME =
 struct
 
 (** evaluation **)
 
 val target = "Eval";
+
+val truth_struct = "Code_Truth";
 
 fun value some_target cookie postproc thy t args =
   let
     val ctxt = ProofContext.init_global thy;
     fun evaluator naming program ((_, (_, ty)), t) deps =

   in
     thy
     |> process result module_name some_file
   end;
 
-val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const;
+val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I);
 val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
 
 
 (** Isar setup **)