tuned

--- a/src/HOL/Int.thy	Fri Nov 07 08:57:15 2008 +0100
+++ b/src/HOL/Int.thy	Mon Nov 10 08:18:56 2008 +0100
@@ -782,11 +782,11 @@
 instantiation int :: number_ring
 begin
 
-definition
-  int_number_of_def [code del]: "number_of w = (of_int w \<Colon> int)"
+definition int_number_of_def [code del]:
+  "number_of w = (of_int w \<Colon> int)"
 
-instance
-  by intro_classes (simp only: int_number_of_def)
+instance proof
+qed (simp only: int_number_of_def)
 
 end
 

--- a/src/Tools/code/code_funcgr.ML	Fri Nov 07 08:57:15 2008 +0100
+++ b/src/Tools/code/code_funcgr.ML	Mon Nov 10 08:18:56 2008 +0100
@@ -14,8 +14,8 @@
   val all: T -> string list
   val pretty: theory -> T -> Pretty.T
   val make: theory -> string list -> T
-  val eval_conv: theory -> (term -> term * (T -> term -> thm)) -> cterm -> thm
-  val eval_term: theory -> (term -> term * (T -> term -> 'a)) -> term -> 'a
+  val eval_conv: theory -> (term -> term * (T -> thm)) -> cterm -> thm
+  val eval_term: theory -> (term -> term * (T -> 'a)) -> term -> 'a
   val timing: bool ref
 end
 
@@ -218,42 +218,42 @@
 
 val ensure_consts = ensure_consts;
 
-fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr =
+fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct funcgr =
   let
     val ct = cterm_of proto_ct;
     val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
     val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
-    fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
-      t [];
+    fun consts_of t =
+      fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
     val algebra = Code.coregular_algebra thy;
     val thm = Code.preprocess_conv thy ct;
     val ct' = Thm.rhs_of thm;
     val t' = Thm.term_of ct';
     val consts = map fst (consts_of t');
     val funcgr' = ensure_consts thy algebra consts funcgr;
-    val (t'', evaluator') = apsnd evaluator_fr (evaluator t');
+    val (t'', evaluator_funcgr) = evaluator t';
     val consts' = consts_of t'';
     val dicts = instances_of_consts thy algebra funcgr' consts';
     val funcgr'' = ensure_consts thy algebra dicts funcgr';
-  in (evaluator' thm funcgr'' t'', funcgr'') end;
+  in (evaluator_lift evaluator_funcgr thm funcgr'', funcgr'') end;
 
 fun proto_eval_conv thy =
   let
-    fun evaluator evaluator' thm1 funcgr t =
+    fun evaluator_lift evaluator thm1 funcgr =
       let
-        val thm2 = evaluator' funcgr t;
+        val thm2 = evaluator funcgr;
         val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
       in
         Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
           error ("could not construct evaluation proof:\n"
           ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
       end;
-  in proto_eval thy I evaluator end;
+  in proto_eval thy I evaluator_lift end;
 
 fun proto_eval_term thy =
   let
-    fun evaluator evaluator' _ funcgr t = evaluator' funcgr t;
-  in proto_eval thy (Thm.cterm_of thy) evaluator end;
+    fun evaluator_lift evaluator _ funcgr = evaluator funcgr;
+  in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
 
 end; (*local*)
 

--- a/src/Tools/code/code_ml.ML	Fri Nov 07 08:57:15 2008 +0100
+++ b/src/Tools/code/code_ml.ML	Mon Nov 10 08:18:56 2008 +0100
@@ -8,9 +8,9 @@
 signature CODE_ML =
 sig
   val eval_conv: string * (unit -> thm) option ref
-    -> theory -> cterm -> string list -> thm;
+    -> theory -> cterm -> string list -> thm
   val eval_term: string * (unit -> 'a) option ref
-    -> theory -> term -> string list -> 'a;
+    -> theory -> term -> string list -> 'a
   val setup: theory -> theory
 end;
 
@@ -893,7 +893,7 @@
     fun eval' naming program ((vs, ty), t) deps =
       let
         val _ = if Code_Thingol.contains_dictvar t then
-          error "Term to be evaluated constains free dictionaries" else ();
+          error "Term to be evaluated contains free dictionaries" else ();
         val value_name = "Value.VALUE.value"
         val program' = program
           |> Graph.new_node (value_name,
@@ -903,7 +903,7 @@
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
       in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
-  in eval'' thy (fn t => (t, eval')) ct end;
+  in eval'' thy (rpair eval') ct end;
 
 fun eval_conv reff = eval Code_Thingol.eval_conv Thm.term_of reff;
 fun eval_term reff = eval Code_Thingol.eval_term I reff;

--- a/src/Tools/code/code_thingol.ML	Fri Nov 07 08:57:15 2008 +0100
+++ b/src/Tools/code/code_thingol.ML	Mon Nov 10 08:18:56 2008 +0100
@@ -449,6 +449,8 @@
 
 (** translation kernel **)
 
+(* generic mechanisms *)
+
 fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
   let
     fun add_dep name = case dep of NONE => I
@@ -482,6 +484,9 @@
       ^ Syntax.string_of_sort_global thy sort;
   in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
 
+
+(* translation *)
+
 fun ensure_class thy (algbr as (_, algebra)) funcgr class =
   let
     val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
@@ -713,8 +718,6 @@
   | NONE => translate_app_default thy algbr funcgr thm ((c, ty), ts);
 
 
-(** generated programs **)
-
 (* store *)
 
 structure Program = CodeDataFun
@@ -733,7 +736,7 @@
 
 val cached_program = Program.get;
 
-fun generate thy funcgr f name =
+fun invoke_generation thy funcgr f name =
   Program.change_yield thy (fn naming_program => (NONE, naming_program)
     |> f thy (Code.operational_algebra thy) funcgr name
     |-> (fn name => fn (_, naming_program) => (name, naming_program)));
@@ -750,7 +753,7 @@
     fun generate_consts thy algebra funcgr =
       fold_map (ensure_const thy algebra funcgr);
   in
-    generate thy (Code_Funcgr.make thy cs) generate_consts cs
+    invoke_generation thy (Code_Funcgr.make thy cs) generate_consts cs
     |-> project_consts
   end;
 
@@ -783,20 +786,17 @@
     #> term_value
   end;
 
-fun eval eval_kind thy evaluator =
+fun eval thy evaluator t =
   let
-    fun evaluator'' evaluator''' funcgr t =
+    val (t', evaluator'') = evaluator t;
+    fun evaluator' funcgr =
       let
-        val (((naming, program), (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t;
-      in evaluator''' naming program vs_ty_t deps end;
-    fun evaluator' t =
-      let
-        val (t', evaluator''') = evaluator t;
-      in (t', evaluator'' evaluator''') end;
-  in eval_kind thy evaluator' end
+        val (((naming, program), (vs_ty_t, deps)), _) = invoke_generation thy funcgr ensure_value t';
+      in evaluator'' naming program vs_ty_t deps end;
+  in (t', evaluator') end
 
-fun eval_conv thy = eval Code_Funcgr.eval_conv thy;
-fun eval_term thy = eval Code_Funcgr.eval_term thy;
+fun eval_conv thy = Code_Funcgr.eval_conv thy o eval thy;
+fun eval_term thy = Code_Funcgr.eval_term thy o eval thy;
 
 end; (*struct*)