merged

--- a/src/HOL/Tools/hologic.ML	Tue Dec 21 15:00:59 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Tue Dec 21 16:41:31 2010 +0100
@@ -8,7 +8,7 @@
 sig
   val typeS: sort
   val typeT: typ
-  val mk_id: typ -> term
+  val id_const: typ -> term
   val mk_comp: term * term -> term
   val boolN: string
   val boolT: typ
@@ -146,7 +146,7 @@
 
 (* functions *)
 
-fun mk_id T = Const ("Fun.id", T --> T);
+fun id_const T = Const ("Fun.id", T --> T);
 
 fun mk_comp (f, g) =
   let

--- a/src/Tools/Code/code_target.ML	Tue Dec 21 15:00:59 2010 +0100
+++ b/src/Tools/Code/code_target.ML	Tue Dec 21 16:41:31 2010 +0100
@@ -410,7 +410,7 @@
     else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
   end;
 
-fun evaluation mounted_serializer prepared_program deps ((vs, ty), t) =
+fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) =
   let
     val _ = if Code_Thingol.contains_dict_var t then
       error "Term to be evaluated contains free dictionaries" else ();
@@ -421,16 +421,16 @@
     val program = prepared_program
       |> Graph.new_node (value_name,
           Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
-      |> fold (curry (perhaps o try o Graph.add_edge) value_name) deps;
+      |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
     val (program_code, deresolve) = produce (mounted_serializer program);
     val value_name' = the (deresolve value_name);
   in (program_code, value_name') end;
 
-fun evaluator thy target naming program deps =
+fun evaluator thy target naming program consts =
   let
     val (mounted_serializer, prepared_program) = mount_serializer thy
-      target NONE "Code" [] naming program deps;
-  in evaluation mounted_serializer prepared_program deps end;
+      target NONE "Code" [] naming program consts;
+  in evaluation mounted_serializer prepared_program consts end;
 
 end; (* local *)
 

--- a/src/Tools/Code/code_thingol.ML	Tue Dec 21 15:00:59 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Dec 21 16:41:31 2010 +0100
@@ -912,31 +912,37 @@
 fun dynamic_value thy postproc evaluator =
   Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
 
-fun provide_program thy consts f algebra eqngr =
-  let
-    fun generate_consts thy algebra eqngr =
-      fold_map (ensure_const thy algebra eqngr false);
-    val (consts', (naming, program)) = invoke_generation true thy (algebra, eqngr)
-      generate_consts consts;
-  in f algebra eqngr naming program consts' end;
-
-fun static_evaluation thy evaluator algebra eqngr naming program consts' vs t =
+fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
   let
     val (((_, program'), (((vs', ty'), t'), deps)), _) =
       ensure_value thy algebra eqngr t (NONE, (naming, program));
-  in evaluator naming program' consts' ((original_sorts vs vs', (vs', ty')), t') deps end;
+  in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
+
+fun lift_evaluator thy evaluator' consts algebra eqngr =
+  let
+    fun generate_consts thy algebra eqngr =
+      fold_map (ensure_const thy algebra eqngr false);
+    val (consts', (naming, program)) =
+      invoke_generation true thy (algebra, eqngr) generate_consts consts;
+    val evaluation' = evaluator' naming program consts';
+  in lift_evaluation thy evaluation' algebra eqngr naming program end;
+
+fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
+  let
+    fun generate_consts thy algebra eqngr =
+      fold_map (ensure_const thy algebra eqngr false);
+    val (consts', (naming, program)) =
+      invoke_generation true thy (algebra, eqngr) generate_consts consts;
+  in evaluator' program end;
 
 fun static_conv thy consts conv =
-  Code_Preproc.static_conv thy consts
-    (provide_program thy consts (static_evaluation thy conv));
+  Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts);
 
 fun static_conv_simple thy consts conv =
-  Code_Preproc.static_conv thy consts
-    (provide_program thy consts (fn _ => fn _ => fn _ => fn program => fn _ => conv program));
+  Code_Preproc.static_conv thy consts (lift_evaluator_simple thy conv consts);
 
 fun static_value thy postproc consts evaluator =
-  Code_Preproc.static_value thy postproc consts
-    (provide_program thy consts (static_evaluation thy evaluator));
+  Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
 
 
 (** diagnostic commands **)