# HG changeset patch
# User haftmann
# Date 1284562591 -7200
# Node ID 9019b6afaa4a9ddf673c59d16a5d7260198b0a2a
# Parent  b6a77cffc231667e55766f0744b68929058d5538
proper interface for code_reflect

diff -r b6a77cffc231 -r 9019b6afaa4a src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Sep 15 16:47:31 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Wed Sep 15 16:56:31 2010 +0200
@@ -10,6 +10,8 @@
   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;
 
@@ -20,6 +22,8 @@
 
 val target = "Eval";
 
+val truth_struct = "Code_Truth";
+
 fun value some_target cookie postproc thy t args =
   let
     val ctxt = ProofContext.init_global thy;
@@ -184,7 +188,7 @@
     |> 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;