canonical handling of theory context argument

--- a/src/Tools/Code/code_preproc.ML	Tue Dec 21 08:40:39 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Tue Dec 21 09:18:29 2010 +0100
@@ -29,9 +29,9 @@
   val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
   val static_conv: theory -> string list
-    -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
+    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
   val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
-    -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
+    -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
 
   val setup: theory -> theory
 end
@@ -490,7 +490,7 @@
 fun static_conv thy consts conv =
   let
     val (algebra, eqngr) = obtain true thy consts [];
-    val conv' = conv algebra eqngr thy;
+    val conv' = conv algebra eqngr;
   in
     no_variables_conv ((preprocess_conv thy)
       then_conv (fn ct => uncurry conv' (dest_cterm ct) ct)
@@ -504,7 +504,7 @@
   in 
     preprocess_term thy
     #-> (fn resubst => fn t => t
-      |> evaluator' thy (Term.add_tfrees t [])
+      |> evaluator' (Term.add_tfrees t [])
       |> postproc (postprocess_term thy o resubst))
   end;
 

--- a/src/Tools/Code/code_simp.ML	Tue Dec 21 08:40:39 2010 +0100
+++ b/src/Tools/Code/code_simp.ML	Tue Dec 21 09:18:29 2010 +0100
@@ -68,7 +68,7 @@
 
 fun static_conv thy some_ss consts =
   Code_Thingol.static_conv_simple thy consts
-    (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
+    (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
 
 fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
   THEN' conclude_tac thy some_ss;

--- a/src/Tools/Code/code_thingol.ML	Tue Dec 21 08:40:39 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Dec 21 09:18:29 2010 +0100
@@ -100,14 +100,14 @@
   val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
     -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
-  val static_conv: theory -> string list -> (naming -> program
-    -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+  val static_conv: theory -> string list -> (naming -> program -> string list
+    -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
     -> conv
   val static_conv_simple: theory -> string list
-    -> (program -> theory -> (string * sort) list -> term -> conv) -> conv
+    -> (program -> (string * sort) list -> term -> conv) -> conv
   val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
-    (naming -> program
-      -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+    (naming -> program -> string list
+      -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
 end;
 
@@ -916,27 +916,27 @@
   let
     fun generate_consts thy algebra eqngr =
       fold_map (ensure_const thy algebra eqngr false);
-    val (_, (naming, program)) = invoke_generation true thy (algebra, eqngr)
+    val (consts', (naming, program)) = invoke_generation true thy (algebra, eqngr)
       generate_consts consts;
-  in f algebra eqngr naming program end;
+  in f algebra eqngr naming program consts' end;
 
-fun static_evaluator evaluator algebra eqngr naming program thy vs t =
+fun static_evaluation thy evaluator algebra eqngr naming program consts' vs t =
   let
     val (((_, program'), (((vs', ty'), t'), deps)), _) =
       ensure_value thy algebra eqngr t (NONE, (naming, program));
-  in evaluator naming program' thy ((original_sorts vs vs', (vs', ty')), t') deps end;
+  in evaluator naming program' consts' ((original_sorts vs vs', (vs', ty')), t') deps end;
 
 fun static_conv thy consts conv =
   Code_Preproc.static_conv thy consts
-    (provide_program thy consts (static_evaluator conv));
+    (provide_program thy consts (static_evaluation thy conv));
 
 fun static_conv_simple thy consts conv =
   Code_Preproc.static_conv thy consts
-    (provide_program thy consts ((K o K o K) conv));
+    (provide_program thy consts (fn _ => fn _ => fn _ => fn program => fn _ => conv program));
 
 fun static_value thy postproc consts evaluator =
   Code_Preproc.static_value thy postproc consts
-    (provide_program thy consts (static_evaluator evaluator));
+    (provide_program thy consts (static_evaluation thy evaluator));
 
 
 (** diagnostic commands **)

--- a/src/Tools/nbe.ML	Tue Dec 21 08:40:39 2010 +0100
+++ b/src/Tools/nbe.ML	Tue Dec 21 09:18:29 2010 +0100
@@ -602,13 +602,13 @@
 
 fun static_conv thy consts =
   lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
-    (K (fn program => let val nbe_program = compile true thy program
-      in fn thy => oracle thy program nbe_program end)));
+    (K (fn program => fn _ => let val nbe_program = compile true thy program
+      in oracle thy program nbe_program end)));
 
 fun static_value thy consts = lift_triv_classes_rew thy
   (Code_Thingol.static_value thy I consts
-    (K (fn program => let val nbe_program = compile true thy program
-      in fn thy => eval_term thy program (compile false thy program) end)));
+    (K (fn program => fn _ => let val nbe_program = compile true thy program
+      in eval_term thy program (compile false thy program) end)));
 
 
 (** setup **)