# HG changeset patch
# User haftmann
# Date 1186472434 -7200
# Node ID 7b28dc69bdbb015d940928619eb102396685dece
# Parent  605f664d5115ceb7ac0d7a6b8cce18de0553cce5
new nbe implementation

diff -r 605f664d5115 -r 7b28dc69bdbb src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/HOL/HOL.thy	Tue Aug 07 09:40:34 2007 +0200
@@ -25,6 +25,7 @@
   "~~/src/Provers/quantifier1.ML"
   ("simpdata.ML")
   ("~~/src/HOL/Tools/recfun_codegen.ML")
+  "~~/src/Tools/nbe.ML"
 begin
 
 subsection {* Primitive logic *}
@@ -1540,6 +1541,12 @@
 
 subsection {* Other simple lemmas and lemma duplicates *}
 
+lemma Let_0 [simp]: "Let 0 f = f 0"
+  unfolding Let_def ..
+
+lemma Let_1 [simp]: "Let 1 f = f 1"
+  unfolding Let_def ..
+
 lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
   by blast+
 
@@ -1786,9 +1793,13 @@
   (OCaml "failwith/ \"undefined\"")
   (Haskell "error/ \"undefined\"")
 
-code_reserved SML Fail
-code_reserved OCaml failwith
+
+text {* Let and If *}
 
+setup {*
+  CodegenPackage.add_appconst (@{const_name Let}, CodegenPackage.appgen_let)
+  #> CodegenPackage.add_appconst (@{const_name If}, CodegenPackage.appgen_if)
+*}
 
 subsubsection {* Evaluation oracle *}
 
@@ -1811,31 +1822,15 @@
 
 subsubsection {* Normalization by evaluation *}
 
+setup Nbe.setup
+
 method_setup normalization = {*
   Method.no_args (Method.SIMPLE_METHOD'
-    (CONVERSION (ObjectLogic.judgment_conv NBE.normalization_conv)
+    (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
       THEN' resolve_tac [TrueI, refl]))
 *} "solve goal by normalization"
 
 
-text {* lazy @{const If} *}
-
-definition
-  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  [code func del]: "if_delayed b f g = (if b then f True else g False)"
-
-lemma [code func]:
-  shows "if_delayed True f g = f True"
-    and "if_delayed False f g = g False"
-  unfolding if_delayed_def by simp_all
-
-lemma [normal pre, symmetric, normal post]:
-  "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
-  unfolding if_delayed_def ..
-
-hide (open) const if_delayed
-
-
 subsection {* Legacy tactics and ML bindings *}
 
 ML {*
diff -r 605f664d5115 -r 7b28dc69bdbb src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/HOL/List.thy	Tue Aug 07 09:40:34 2007 +0200
@@ -757,9 +757,9 @@
 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
 by (induct xs) auto
 
-lemma set_allpairs[simp]:
+lemma set_allpairs [simp]:
  "set(allpairs f xs ys) = {z. EX x : set xs. EX y : set ys. z = f x y}"
-by(induct xs) auto
+by (induct xs) auto
 
 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
 by (induct xs) auto
@@ -2923,7 +2923,7 @@
   show ?case by (induct xs) (auto simp add: Cons aux)
 qed
 
-lemma mem_iff [normal post]:
+lemma mem_iff [code post]:
   "x mem xs \<longleftrightarrow> x \<in> set xs"
   by (induct xs) auto
 
@@ -2933,14 +2933,14 @@
   "xs = [] \<longleftrightarrow> null xs"
   by (cases xs) simp_all
 
-lemmas null_empty [normal post] =
+lemmas null_empty [code post] =
   empty_null [symmetric]
 
 lemma list_inter_conv:
   "set (list_inter xs ys) = set xs \<inter> set ys"
   by (induct xs) auto
 
-lemma list_all_iff [normal post]:
+lemma list_all_iff [code post]:
   "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
   by (induct xs) auto
 
@@ -2958,7 +2958,7 @@
   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
   unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
 
-lemma list_ex_iff [normal post]:
+lemma list_ex_iff [code post]:
   "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
   by (induct xs) simp_all
 
@@ -2978,7 +2978,7 @@
   by (induct xs) auto
 
 lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs"
-by(simp add:listsum_foldr foldl_map[symmetric] foldl_foldr1)
+  by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1)
 
 
 text {* Code for bounded quantification over nats. *}
diff -r 605f664d5115 -r 7b28dc69bdbb src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/HOL/Numeral.thy	Tue Aug 07 09:40:34 2007 +0200
@@ -36,11 +36,11 @@
 
 definition
   Pls :: int where
-  [code func del]:"Pls = 0"
+  [code func del]: "Pls = 0"
 
 definition
   Min :: int where
-  [code func del]:"Min = - 1"
+  [code func del]: "Min = - 1"
 
 definition
   Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
@@ -67,12 +67,6 @@
   -- {* Unfold all @{text let}s involving constants *}
   unfolding Let_def ..
 
-lemma Let_0 [simp]: "Let 0 f = f 0"
-  unfolding Let_def ..
-
-lemma Let_1 [simp]: "Let 1 f = f 1"
-  unfolding Let_def ..
-
 definition
   succ :: "int \<Rightarrow> int" where
   [code func del]: "succ k = k + 1"
@@ -94,11 +88,11 @@
 
 text {* Removal of leading zeroes *}
 
-lemma Pls_0_eq [simp, normal post]:
+lemma Pls_0_eq [simp, code post]:
   "Pls BIT B0 = Pls"
   unfolding numeral_simps by simp
 
-lemma Min_1_eq [simp, normal post]:
+lemma Min_1_eq [simp, code post]:
   "Min BIT B1 = Min"
   unfolding numeral_simps by simp
 
@@ -613,11 +607,11 @@
 lemma [code]: "nat i = nat_aux i 0"
   by (simp add: nat_aux_def)
 
-lemma zero_is_num_zero [code func, code inline, symmetric, normal post]:
+lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
   "(0\<Colon>int) = Numeral0" 
   by simp
 
-lemma one_is_num_one [code func, code inline, symmetric, normal post]:
+lemma one_is_num_one [code func, code inline, symmetric, code post]:
   "(1\<Colon>int) = Numeral1" 
   by simp 
 
diff -r 605f664d5115 -r 7b28dc69bdbb src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/IsaMakefile	Tue Aug 07 09:40:34 2007 +0200
@@ -63,7 +63,7 @@
   Tools/codegen_consts.ML Tools/codegen_data.ML Tools/codegen_func.ML		\
   Tools/codegen_funcgr.ML Tools/codegen_names.ML Tools/codegen_package.ML	\
   Tools/codegen_serializer.ML Tools/codegen_thingol.ML Tools/invoke.ML		\
-  Tools/named_thms.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML	\
+  Tools/named_thms.ML	\
   Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML		\
   compress.ML config.ML conjunction.ML consts.ML context.ML context_position.ML	\
   conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML library.ML	\
diff -r 605f664d5115 -r 7b28dc69bdbb src/Pure/Tools/ROOT.ML
--- a/src/Pure/Tools/ROOT.ML	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/ROOT.ML	Tue Aug 07 09:40:34 2007 +0200
@@ -22,8 +22,3 @@
 use "codegen_thingol.ML";
 use "codegen_serializer.ML";
 use "codegen_package.ML";
-
-(*norm-by-eval*)
-use "nbe_eval.ML";
-use "nbe_codegen.ML";
-use "nbe.ML";
diff -r 605f664d5115 -r 7b28dc69bdbb src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Tue Aug 07 09:40:34 2007 +0200
@@ -21,6 +21,8 @@
   val del_inline_proc: string -> theory -> theory
   val add_preproc: string * (theory -> thm list -> thm list) -> theory -> theory
   val del_preproc: string -> theory -> theory
+  val add_post: thm -> theory -> theory
+  val del_post: thm -> theory -> theory
   val add_datatype: string * ((string * sort) list * (string * typ list) list)
     -> theory -> theory
   val add_datatype_consts: CodegenConsts.const list -> theory -> theory
@@ -33,7 +35,8 @@
   val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
   val default_typ: theory -> CodegenConsts.const -> typ
 
-  val preprocess_cterm: cterm -> thm
+  val preprocess_conv: cterm -> thm
+  val postprocess_conv: cterm -> thm
 
   val print_codesetup: theory -> unit
 
@@ -176,24 +179,29 @@
 
 (** exeuctable content **)
 
-datatype preproc = Preproc of {
+datatype thmproc = Preproc of {
   inlines: thm list,
   inline_procs: (string * (serial * (theory -> cterm list -> thm list))) list,
-  preprocs: (string * (serial * (theory -> thm list -> thm list))) list
+  preprocs: (string * (serial * (theory -> thm list -> thm list))) list,
+  posts: thm list
 };
 
-fun mk_preproc ((inlines, inline_procs), preprocs) =
-  Preproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs };
-fun map_preproc f (Preproc { inlines, inline_procs, preprocs }) =
-  mk_preproc (f ((inlines, inline_procs), preprocs));
-fun merge_preproc (Preproc { inlines = inlines1, inline_procs = inline_procs1, preprocs = preprocs1 },
-  Preproc { inlines = inlines2, inline_procs = inline_procs2, preprocs = preprocs2 }) =
+fun mk_thmproc (((inlines, inline_procs), preprocs), posts) =
+  Preproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs,
+    posts = posts };
+fun map_thmproc f (Preproc { inlines, inline_procs, preprocs, posts }) =
+  mk_thmproc (f (((inlines, inline_procs), preprocs), posts));
+fun merge_thmproc (Preproc { inlines = inlines1, inline_procs = inline_procs1,
+    preprocs = preprocs1, posts = posts1 },
+  Preproc { inlines = inlines2, inline_procs = inline_procs2,
+      preprocs = preprocs2, posts= posts2 }) =
     let
       val (touched1, inlines) = merge_thms (inlines1, inlines2);
       val (touched2, inline_procs) = merge_alist (op =) (eq_fst (op =)) (inline_procs1, inline_procs2);
       val (touched3, preprocs) = merge_alist (op =) (eq_fst (op =)) (preprocs1, preprocs2);
+      val (_, posts) = merge_thms (posts1, posts2);
     in (touched1 orelse touched2 orelse touched3,
-      mk_preproc ((inlines, inline_procs), preprocs)) end;
+      mk_thmproc (((inlines, inline_procs), preprocs), posts)) end;
 
 fun join_func_thms (tabs as (tab1, tab2)) =
   let
@@ -246,29 +254,29 @@
   in (touched, mk_spec (funcs, dtyps)) end;
 
 datatype exec = Exec of {
-  preproc: preproc,
+  thmproc: thmproc,
   spec: spec
 };
 
-fun mk_exec (preproc, spec) =
-  Exec { preproc = preproc, spec = spec };
-fun map_exec f (Exec { preproc = preproc, spec = spec }) =
-  mk_exec (f (preproc, spec));
-fun merge_exec (Exec { preproc = preproc1, spec = spec1 },
-  Exec { preproc = preproc2, spec = spec2 }) =
+fun mk_exec (thmproc, spec) =
+  Exec { thmproc = thmproc, spec = spec };
+fun map_exec f (Exec { thmproc = thmproc, spec = spec }) =
+  mk_exec (f (thmproc, spec));
+fun merge_exec (Exec { thmproc = thmproc1, spec = spec1 },
+  Exec { thmproc = thmproc2, spec = spec2 }) =
   let
-    val (touched', preproc) = merge_preproc (preproc1, preproc2);
+    val (touched', thmproc) = merge_thmproc (thmproc1, thmproc2);
     val (touched_cs, spec) = merge_spec (spec1, spec2);
     val touched = if touched' then NONE else touched_cs;
-  in (touched, mk_exec (preproc, spec)) end;
-val empty_exec = mk_exec (mk_preproc (([], []), []),
+  in (touched, mk_exec (thmproc, spec)) end;
+val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
   mk_spec (Consttab.empty, Symtab.empty));
 
-fun the_preproc (Exec { preproc = Preproc x, ...}) = x;
+fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x;
 fun the_spec (Exec { spec = Spec x, ...}) = x;
 val the_funcs = #funcs o the_spec;
 val the_dtyps = #dtyps o the_spec;
-val map_preproc = map_exec o apfst o map_preproc;
+val map_thmproc = map_exec o apfst o map_thmproc;
 val map_funcs = map_exec o apsnd o map_spec o apfst;
 val map_dtyps = map_exec o apsnd o map_spec o apsnd;
 
@@ -404,9 +412,9 @@
                      (Pretty.block o Pretty.breaks)
                         (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
           );
-    val inlines = (#inlines o the_preproc) exec;
-    val inline_procs = (map fst o #inline_procs o the_preproc) exec;
-    val preprocs = (map fst o #preprocs o the_preproc) exec;
+    val inlines = (#inlines o the_thmproc) exec;
+    val inline_procs = (map fst o #inline_procs o the_thmproc) exec;
+    val preprocs = (map fst o #preprocs o the_thmproc) exec;
     val funs = the_funcs exec
       |> Consttab.dest
       |> (map o apfst) (CodegenConsts.string_of_const thy)
@@ -695,32 +703,43 @@
 end; (*local*)
 
 fun add_inline thm thy =
-  (map_exec_purge NONE o map_preproc o apfst o apfst)
+  (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
     (insert Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
         (*fully applied in order to get right context for mk_rew!*)
 
 fun del_inline thm thy =
-  (map_exec_purge NONE o map_preproc o apfst o apfst)
+  (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
     (remove Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
         (*fully applied in order to get right context for mk_rew!*)
 
 fun add_inline_proc (name, f) =
-  (map_exec_purge NONE o map_preproc o apfst o apsnd)
+  (map_exec_purge NONE o map_thmproc o apfst o apfst o apsnd)
     (AList.update (op =) (name, (serial (), f)));
 
 fun del_inline_proc name =
-  (map_exec_purge NONE o map_preproc o apfst o apsnd)
+  (map_exec_purge NONE o map_thmproc o apfst o apfst o apsnd)
     (delete_force "inline procedure" name);
 
 fun add_preproc (name, f) =
-  (map_exec_purge NONE o map_preproc o apsnd) (AList.update (op =) (name, (serial (), f)));
+  (map_exec_purge NONE o map_thmproc o apfst o apsnd)
+    (AList.update (op =) (name, (serial (), f)));
 
 fun del_preproc name =
-  (map_exec_purge NONE o map_preproc o apsnd) (delete_force "preprocessor" name);
+  (map_exec_purge NONE o map_thmproc o apfst o apsnd)
+    (delete_force "preprocessor" name);
+
+fun add_post thm thy =
+  (map_exec_purge NONE o map_thmproc o apsnd)
+    (insert Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
+        (*fully applied in order to get right context for mk_rew!*)
+
+fun del_post thm thy =
+  (map_exec_purge NONE o map_thmproc o apsnd)
+    (remove Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
+        (*fully applied in order to get right context for mk_rew!*)
 
 
-
-(** retrieval **)
+(** , post- and preprocessing **)
 
 local
 
@@ -752,20 +771,28 @@
 
 fun preprocess thy thms =
   thms
-  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_preproc o get_exec) thy)
-  |> map (CodegenFunc.rewrite_func ((#inlines o the_preproc o get_exec) thy))
-  |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy)
+  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o get_exec) thy)
+  |> map (CodegenFunc.rewrite_func ((#inlines o the_thmproc o get_exec) thy))
+  |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o get_exec) thy)
 (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
   |> common_typ_funcs;
 
-fun preprocess_cterm ct =
+fun preprocess_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
   in
     ct
-    |> MetaSimplifier.rewrite false ((#inlines o the_preproc o get_exec) thy)
+    |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o get_exec) thy)
     |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
-        ((#inline_procs o the_preproc o get_exec) thy)
+        ((#inline_procs o the_thmproc o get_exec) thy)
+  end;
+
+fun postprocess_conv ct =
+  let
+    val thy = Thm.theory_of_cterm ct;
+  in
+    ct
+    |> MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy)
   end;
 
 end; (*local*)
diff -r 605f664d5115 -r 7b28dc69bdbb src/Pure/Tools/codegen_funcgr.ML
--- a/src/Pure/Tools/codegen_funcgr.ML	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML	Tue Aug 07 09:40:34 2007 +0200
@@ -24,6 +24,10 @@
   val make: theory -> CodegenConsts.const list -> T
   val make_consts: theory -> CodegenConsts.const list -> CodegenConsts.const list * T
   val make_term: theory -> (T -> (thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T
+    (*FIXME drop make_term as soon as possible*)
+  val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
+  val intervene: theory -> T -> T
+    (*FIXME drop intervene as soon as possible*)
 end;
 
 structure CodegenFuncgr = (*signature is added later*)
@@ -317,7 +321,7 @@
       in Thm.transitive thm thm' end
     val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
     val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
-    val thm1 = CodegenData.preprocess_cterm ct
+    val thm1 = CodegenData.preprocess_conv ct
       |> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy);
     val ct' = Thm.rhs_of thm1;
     val consts = consts_of thy (Thm.term_of ct');
@@ -343,6 +347,20 @@
     val funcgr'' = ensure_consts rewrites thy instdefs funcgr';
   in (f funcgr'' drop ct'' thm5, funcgr'') end;
 
+fun ensure_consts_eval rewrites thy conv =
+  let
+    fun conv' funcgr drop_classes ct thm1 =
+      let
+        val thm2 = conv funcgr ct;
+        val thm3 = CodegenData.postprocess_conv (Thm.rhs_of thm2);
+        val thm23 = drop_classes (Thm.transitive thm2 thm3);
+      in
+        Thm.transitive thm1 thm23 handle THM _ =>
+          error ("eval_conv - could not construct proof:\n"
+          ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
+      end;
+  in ensure_consts_term rewrites thy conv' end;
+
 end; (*local*)
 
 end; (*struct*)
@@ -374,6 +392,13 @@
 fun make_term thy f =
   Funcgr.change_yield thy o CodegenFuncgr.ensure_consts_term rewrites thy f;
 
+fun eval_conv thy f =
+  fst o Funcgr.change_yield thy o CodegenFuncgr.ensure_consts_eval rewrites thy f;
+
+(*FIXME*)
+fun intervene thy funcgr =
+  Funcgr.change thy (K funcgr);
+
 end; (*functor*)
 
 structure CodegenFuncgr : CODEGEN_FUNCGR =
diff -r 605f664d5115 -r 7b28dc69bdbb src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Tue Aug 07 09:40:34 2007 +0200
@@ -7,16 +7,21 @@
 
 signature CODEGEN_PACKAGE =
 sig
-  val compile_term: theory -> term -> CodegenThingol.code * CodegenThingol.iterm;
+  (* interfaces *)
+  val eval_conv: theory
+    -> (CodegenThingol.code -> CodegenThingol.iterm -> cterm -> thm) -> cterm -> thm;
+  val codegen_command: theory -> string -> unit;
+
+  (* primitive interfaces *)
   val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a;
   val satisfies_ref: bool option ref;
   val satisfies: theory -> term -> string list -> bool;
-  val codegen_command: theory -> string -> unit;
 
-  (*axiomatic interfaces*)
+  (* axiomatic interfaces *)
   type appgen;
   val add_appconst: string * appgen -> theory -> theory;
   val appgen_let: appgen;
+  val appgen_if: appgen;
   val appgen_case: (theory -> term
     -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
     -> appgen;
@@ -125,7 +130,7 @@
     val classops' = map (CodegenNames.const thy o CodegenConsts.const_of_cexpr thy) cs;
     val defgen_class =
       fold_map (ensure_def_class thy algbr funcgr) superclasses
-      ##>> (fold_map (exprgen_type thy algbr funcgr) o map snd) cs
+      ##>> (fold_map (exprgen_typ thy algbr funcgr) o map snd) cs
       #-> (fn (superclasses, classoptyps) => succeed
         (CodegenThingol.Class (superclasses ~~ classrels', (unprefix "'" v, classops' ~~ classoptyps))))
   in
@@ -148,7 +153,7 @@
             trns
             |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
             ||>> fold_map (fn (c, tys) =>
-              fold_map (exprgen_type thy algbr funcgr) tys
+              fold_map (exprgen_typ thy algbr funcgr) tys
               #-> (fn tys' =>
                 pair ((CodegenNames.const thy o CodegenConsts.const_of_cexpr thy)
                   (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
@@ -165,19 +170,19 @@
   trns
   |> fold_map (ensure_def_class thy algbr funcgr) (proj_sort sort)
   |>> (fn sort => (unprefix "'" v, sort))
-and exprgen_type thy algbr funcgr (TFree vs) trns =
+and exprgen_typ thy algbr funcgr (TFree vs) trns =
       trns
       |> exprgen_tyvar_sort thy algbr funcgr vs
       |>> (fn (v, sort) => ITyVar v)
-  | exprgen_type thy algbr funcgr (Type (tyco, tys)) trns =
+  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) trns =
       case get_abstype thy (tyco, tys)
        of SOME ty =>
             trns
-            |> exprgen_type thy algbr funcgr ty
+            |> exprgen_typ thy algbr funcgr ty
         | NONE =>
             trns
             |> ensure_def_tyco thy algbr funcgr tyco
-            ||>> fold_map (exprgen_type thy algbr funcgr) tys
+            ||>> fold_map (exprgen_typ thy algbr funcgr) tys
             |>> (fn (tyco, tys) => tyco `%% tys);
 
 exception CONSTRAIN of (string * typ) * typ;
@@ -291,7 +296,7 @@
         |> CodegenThingol.message msg (fn trns => trns
         |> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
         ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-        ||>> exprgen_type thy algbr funcgr ty
+        ||>> exprgen_typ thy algbr funcgr ty
         |-> (fn ((eqs, vs), ty) => succeed (CodegenThingol.Fun (eqs, (vs, ty)))))
       end;
     val defgen = if (is_some o CodegenData.get_datatype_of_constr thy) const
@@ -312,14 +317,14 @@
       |> select_appgen thy algbr funcgr ((c, ty), [])
   | exprgen_term thy algbr funcgr (Free (v, ty)) trns =
       trns
-      |> exprgen_type thy algbr funcgr ty
+      |> exprgen_typ thy algbr funcgr ty
       |>> (fn _ => IVar v)
   | exprgen_term thy algbr funcgr (Abs (raw_v, ty, raw_t)) trns =
       let
         val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t);
       in
         trns
-        |> exprgen_type thy algbr funcgr ty
+        |> exprgen_typ thy algbr funcgr ty
         ||>> exprgen_term thy algbr funcgr t
         |>> (fn (ty, t) => (v, ty) `|-> t)
       end
@@ -336,8 +341,8 @@
 and appgen_default thy algbr funcgr ((c, ty), ts) trns =
   trns
   |> ensure_def_const thy algbr funcgr (CodegenConsts.const_of_cexpr thy (c, ty))
-  ||>> fold_map (exprgen_type thy algbr funcgr) ((fst o Term.strip_type) ty)
-  ||>> exprgen_type thy algbr funcgr ((snd o Term.strip_type) ty)
+  ||>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
+  ||>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)
   ||>> exprgen_dict_parms thy algbr funcgr (c, ty)
   ||>> fold_map (exprgen_term thy algbr funcgr) ts
   |>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts)
@@ -353,7 +358,7 @@
             val vs = Name.names ctxt "a" tys;
           in
             trns
-            |> fold_map (exprgen_type thy algbr funcgr) tys
+            |> fold_map (exprgen_typ thy algbr funcgr) tys
             ||>> appgen thy algbr funcgr ((c, ty), ts @ map Free vs)
             |>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
           end
@@ -397,27 +402,37 @@
 (* parametrized application generators, for instantiation in object logic *)
 (* (axiomatic extensions of translation kernel) *)
 
-fun appgen_case dest_case_expr thy algbr funcgr (app as (c_ty, ts)) trns =
+fun appgen_case dest_case_expr thy algbr funcgr (app as (c_ty, ts)) =
   let
     val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
-    fun clausegen (dt, bt) trns =
-      trns
-      |> exprgen_term thy algbr funcgr dt
-      ||>> exprgen_term thy algbr funcgr bt;
+    fun clause_gen (dt, bt) =
+      exprgen_term thy algbr funcgr dt
+      ##>> exprgen_term thy algbr funcgr bt;
   in
-    trns
-    |> exprgen_term thy algbr funcgr st
-    ||>> exprgen_type thy algbr funcgr sty
-    ||>> fold_map clausegen ds
-    |>> (fn ((se, sty), ds) => ICase ((se, sty), ds))
+    exprgen_term thy algbr funcgr st
+    ##>> exprgen_typ thy algbr funcgr sty
+    ##>> fold_map clause_gen ds
+    ##>> appgen_default thy algbr funcgr app
+    #>> (fn (((se, sty), ds), t0) => ICase (((se, sty), ds), t0))
   end;
 
-fun appgen_let thy algbr funcgr (app as (_, [st, ct])) trns =
-  trns
-  |> exprgen_term thy algbr funcgr ct
-  ||>> exprgen_term thy algbr funcgr st
-  |-> (fn ((v, ty) `|-> be, se) => pair (CodegenThingol.collapse_let (((v, ty), se), be))
-        | _ => appgen_default thy algbr funcgr app);
+fun appgen_let thy algbr funcgr (app as (_, [st, ct])) =
+  exprgen_term thy algbr funcgr ct
+  ##>> exprgen_term thy algbr funcgr st
+  ##>> appgen_default thy algbr funcgr app
+  #>> (fn (((v, ty) `|-> be, se), t0) =>
+            ICase (CodegenThingol.collapse_let (((v, ty), se), be), t0)
+        | (_, t0) => t0);
+
+fun appgen_if thy algbr funcgr (app as (_, [tb, tt, tf])) =
+  exprgen_term thy algbr funcgr tb
+  ##>> exprgen_typ thy algbr funcgr (Type ("bool", []))
+  ##>> exprgen_term thy algbr funcgr (Const ("True", Type ("bool", [])))
+  ##>> exprgen_term thy algbr funcgr tt
+  ##>> exprgen_term thy algbr funcgr (Const ("False", Type ("bool", [])))
+  ##>> exprgen_term thy algbr funcgr tf
+  ##>> appgen_default thy algbr funcgr app
+  #>> (fn ((((((tb, B), T), tt), F), tf), t0) => ICase (((tb, B), [(T, tt), (F, tf)]), t0));
 
 fun add_appconst (c, appgen) thy =
   let
@@ -511,6 +526,8 @@
 
 fun generate thy funcgr gen it =
   let
+    (*FIXME*)
+    val _ = Funcgr.intervene thy funcgr;
     val cs = map_filter (Consttab.lookup ((snd o snd o Translation.get) thy))
       (CodegenFuncgr.all funcgr);
     val funcgr' = Funcgr.make thy cs;
@@ -526,6 +543,17 @@
     |> fst
   end;
 
+fun eval_conv thy conv =
+  let
+    fun conv' funcgr ct =
+      let
+        val t = generate thy funcgr exprgen_term' (Thm.term_of ct);
+        val consts = CodegenThingol.fold_constnames (insert (op =)) t [];
+        val code = Code.get thy
+          |> CodegenThingol.project_code true [] (SOME consts)
+      in conv code t ct end;
+  in Funcgr.eval_conv thy conv' end;
+
 fun codegen_term thy t =
   let
     val ct = Thm.cterm_of thy t;
@@ -533,17 +561,6 @@
     val t' = Thm.term_of ct';
   in generate thy funcgr exprgen_term' t' end;
 
-fun compile_term thy t =
-  let
-    val ct = Thm.cterm_of thy t;
-    val (ct', funcgr) = Funcgr.make_term thy (K (K K)) ct;
-    val t' = Thm.term_of ct';
-    val t'' = generate thy funcgr exprgen_term' t';
-    val consts = CodegenThingol.fold_constnames (insert (op =)) t'' [];
-    val code = Code.get thy
-      |> CodegenThingol.project_code true [] (SOME consts)
-  in (code, t'') end;
-
 fun raw_eval_term thy (ref_spec, t) args =
   let
     val _ = (Term.map_types o Term.map_atyps) (fn _ =>
diff -r 605f664d5115 -r 7b28dc69bdbb src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Aug 07 09:40:34 2007 +0200
@@ -281,7 +281,7 @@
       |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
            o fst o dest_name o fst)
              code
-  in (fn name => (the o Symtab.lookup tab) name) end;
+  in fn name => (the o Symtab.lookup tab) name end;
 
 
 
@@ -358,9 +358,30 @@
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (ps @ [pr_term vars' NOBR t']) end
-      | pr_term vars fxy (t as ICase (_, [_])) =
+      | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+                then pr_case vars fxy cases
+                else pr_app vars fxy c_ts
+            | NONE => pr_case vars fxy cases)
+    and pr_app' vars (app as ((c, (iss, tys)), ts)) =
+      if is_cons c then let
+        val k = length tys
+      in if k < 2 then 
+        (str o deresolv) c :: map (pr_term vars BR) ts
+      else if k = length ts then
+        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
+      else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
+        (str o deresolv) c
+          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
+    and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
+    and pr_bind' ((NONE, NONE), _) = str "_"
+      | pr_bind' ((SOME v, NONE), _) = str v
+      | pr_bind' ((NONE, SOME p), _) = p
+      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
+    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
+    and pr_case vars fxy (cases as ((_, [_]), _)) =
           let
-            val (binds, t') = CodegenThingol.unfold_let t;
+            val (binds, t') = CodegenThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
               |> pr_bind NOBR ((NONE, SOME pat), ty)
@@ -373,7 +394,7 @@
               str ("end")
             ]
           end
-      | pr_term vars fxy (ICase ((td, ty), b::bs)) =
+      | pr_case vars fxy (((td, ty), b::bs), _) =
           let
             fun pr delim (pat, t) =
               let
@@ -389,23 +410,7 @@
               :: map (pr "|") bs
             )
           end
-      | pr_term vars fxy (t as ICase (_, [])) = str "raise Fail \"empty case\""
-    and pr_app' vars (app as ((c, (iss, tys)), ts)) =
-      if is_cons c then let
-        val k = length tys
-      in if k < 2 then 
-        (str o deresolv) c :: map (pr_term vars BR) ts
-      else if k = length ts then
-        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
-      else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
-        (str o deresolv) c
-          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
-    and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
-    and pr_bind' ((NONE, NONE), _) = str "_"
-      | pr_bind' ((SOME v, NONE), _) = str v
-      | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
-    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
+      | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""
     fun pr_def (MLFuns (funns as (funn :: funns'))) =
           let
             val definer =
@@ -623,30 +628,11 @@
             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (str "fun" :: ps @ str "->" @@ pr_term vars' NOBR t') end
-      | pr_term vars fxy (t as ICase (_, [_])) =
-          let
-            val (binds, t') = CodegenThingol.unfold_let t;
-            fun pr ((pat, ty), t) vars =
-              vars
-              |> pr_bind NOBR ((NONE, SOME pat), ty)
-              |>> (fn p => concat [str "let", p, str "=", pr_term vars NOBR t, str "in"])
-            val (ps, vars') = fold_map pr binds vars;
-          in Pretty.chunks (ps @| pr_term vars' NOBR t') end
-      | pr_term vars fxy (ICase ((td, ty), b::bs)) =
-          let
-            fun pr delim (pat, t) =
-              let
-                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
-              in concat [str delim, p, str "->", pr_term vars' NOBR t] end;
-          in
-            (Pretty.enclose "(" ")" o single o brackify fxy) (
-              str "match"
-              :: pr_term vars NOBR td
-              :: pr "with" b
-              :: map (pr "|") bs
-            )
-          end
-      | pr_term vars fxy (t as ICase (_, [])) = str "failwith \"empty case\""
+      | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+                then pr_case vars fxy cases
+                else pr_app vars fxy c_ts
+            | NONE => pr_case vars fxy cases)
     and pr_app' vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then
         if length tys = length ts
@@ -662,7 +648,31 @@
       | pr_bind' ((SOME v, NONE), _) = str v
       | pr_bind' ((NONE, SOME p), _) = p
       | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
-    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
+    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
+    and pr_case vars fxy (cases as ((_, [_]), _)) =
+          let
+            val (binds, t') = CodegenThingol.unfold_let (ICase cases);
+            fun pr ((pat, ty), t) vars =
+              vars
+              |> pr_bind NOBR ((NONE, SOME pat), ty)
+              |>> (fn p => concat [str "let", p, str "=", pr_term vars NOBR t, str "in"])
+            val (ps, vars') = fold_map pr binds vars;
+          in Pretty.chunks (ps @| pr_term vars' NOBR t') end
+      | pr_case vars fxy (((td, ty), b::bs), _) =
+          let
+            fun pr delim (pat, t) =
+              let
+                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
+              in concat [str delim, p, str "->", pr_term vars' NOBR t] end;
+          in
+            (Pretty.enclose "(" ")" o single o brackify fxy) (
+              str "match"
+              :: pr_term vars NOBR td
+              :: pr "with" b
+              :: map (pr "|") bs
+            )
+          end
+      | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";
     fun pr_def (MLFuns (funns as funn :: funns')) =
           let
             fun fish_parm _ (w as SOME _) = w
@@ -1123,9 +1133,18 @@
             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (str "\\" :: ps @ str "->" @@ pr_term vars' NOBR t') end
-      | pr_term vars fxy (t as ICase (_, [_])) =
+      | pr_term vars fxy (ICase (cases as (_, t0))) = (case CodegenThingol.unfold_const_app t0
+           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+                then pr_case vars fxy cases
+                else pr_app vars fxy c_ts
+            | NONE => pr_case vars fxy cases)
+    and pr_app' vars ((c, _), ts) =
+      (str o deresolv) c :: map (pr_term vars BR) ts
+    and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
+    and pr_bind fxy = pr_bind_haskell pr_term fxy
+    and pr_case vars fxy (cases as ((_, [_]), _)) =
           let
-            val (binds, t) = CodegenThingol.unfold_let t;
+            val (binds, t) = CodegenThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
               |> pr_bind BR ((NONE, SOME pat), ty)
@@ -1137,7 +1156,7 @@
               concat [str "}", str "in", pr_term vars' NOBR t]
             ) ps
           end
-      | pr_term vars fxy (ICase ((td, ty), bs as _ :: _)) =
+      | pr_case vars fxy (((td, ty), bs as _ :: _), _) =
           let
             fun pr (pat, t) =
               let
@@ -1149,11 +1168,7 @@
               str "})"
             ) (map pr bs)
           end
-      | pr_term vars fxy (t as ICase (_, [])) = str "error \"empty case\""
-    and pr_app' vars ((c, _), ts) =
-      (str o deresolv) c :: map (pr_term vars BR) ts
-    and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars
-    and pr_bind fxy = pr_bind_haskell pr_term fxy;
+      | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
     fun pr_def (name, CodegenThingol.Fun (eqs, (vs, ty))) =
           let
             val tyvars = CodegenNames.intro_vars (map fst vs) init_syms;
@@ -1751,7 +1766,7 @@
   let
     fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
           vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
-            pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
+            pr vars fxy (ICase (((t1, ty), ([(IVar v, t2)])), IVar ""))
       | pretty pr vars fxy [(t1, _), (t2, ty2)] =
           let
             (*this code suffers from the lack of a proper concept for bindings*)
@@ -1760,7 +1775,7 @@
             val vars' = CodegenNames.intro_vars [v] vars;
             val var = IVar v;
             val ty = (hd o fst o CodegenThingol.unfold_fun) ty2;
-          in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
+          in pr vars' fxy (ICase (((t1, ty), ([(var, t2 `$ var)])), IVar "")) end;
   in (2, pretty) end;
 
 end; (*local*)
@@ -2122,7 +2137,7 @@
       ]))
   #> fold (add_reserved "SML") ML_Syntax.reserved_names
   #> fold (add_reserved "SML")
-      ["o" (*dictionary projections use it already*), "div", "mod" (*standard infixes*)]
+      ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
   #> fold (add_reserved "OCaml") [
       "and", "as", "assert", "begin", "class",
       "constraint", "do", "done", "downto", "else", "end", "exception",
@@ -2130,8 +2145,9 @@
       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
       "sig", "struct", "then", "to", "true", "try", "type", "val",
-      "virtual", "when", "while", "with", "mod"
+      "virtual", "when", "while", "with"
     ]
+  #> fold (add_reserved "OCaml") ["failwith", "mod"]
   #> fold (add_reserved "Haskell") [
       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
       "import", "default", "forall", "let", "in", "class", "qualified", "data",
diff -r 605f664d5115 -r 7b28dc69bdbb src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue Aug 07 09:40:34 2007 +0200
@@ -27,9 +27,8 @@
     | IVar of vname
     | `$ of iterm * iterm
     | `|-> of (vname * itype) * iterm
-    | ICase of (iterm * itype) * (iterm * iterm) list;
-        (*(discriminendum term (td), discriminendum type (ty)),
-                [(selector pattern (p), body term (t))] (bs))*)
+    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
+        (*((term, type), [(selector pattern, body term )]), primitive term)*)
   val `-> : itype * itype -> itype;
   val `--> : itype list * itype -> itype;
   val `$$ : iterm * iterm list -> iterm;
@@ -50,7 +49,8 @@
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
   val unfold_const_app: iterm ->
     ((string * (dict list list * itype list)) * iterm list) option;
-  val collapse_let: ((vname * itype) * iterm) * iterm -> iterm;
+  val collapse_let: ((vname * itype) * iterm) * iterm
+    -> (iterm * itype) * (iterm * iterm) list;
   val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
   val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
@@ -129,7 +129,7 @@
   | IVar of vname
   | `$ of iterm * iterm
   | `|-> of (vname * itype) * iterm
-  | ICase of (iterm * itype) * (iterm * iterm) list;
+  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
     (*see also signature*)
 
 (*
@@ -171,7 +171,7 @@
     | _ => NONE);
 
 val split_abs =
-  (fn (v, ty) `|-> (t as ICase ((IVar w, _), [(p, t')])) =>
+  (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
         if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
     | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
     | _ => NONE);
@@ -179,7 +179,7 @@
 val unfold_abs = unfoldr split_abs;
 
 val split_let = 
-  (fn ICase ((td, ty), [(p, t)]) => SOME (((p, ty), td), t)
+  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
     | _ => NONE);
 
 val unfold_let = unfoldr split_let;
@@ -189,16 +189,11 @@
   of (IConst c, ts) => SOME (c, ts)
    | _ => NONE;
 
-fun fold_aiterms f (t as IConst _) =
-      f t
-  | fold_aiterms f (t as IVar _) =
-      f t
-  | fold_aiterms f (t1 `$ t2) =
-      fold_aiterms f t1 #> fold_aiterms f t2
-  | fold_aiterms f (t as _ `|-> t') =
-      f t #> fold_aiterms f t'
-  | fold_aiterms f (ICase ((td, _), bs)) =
-      fold_aiterms f td #> fold (fn (p, t) => fold_aiterms f p #> fold_aiterms f t) bs;
+fun fold_aiterms f (t as IConst _) = f t
+  | fold_aiterms f (t as IVar _) = f t
+  | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
+  | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
+  | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
 
 fun fold_constnames f =
   let
@@ -215,29 +210,24 @@
 
 fun fold_unbound_varnames f =
   let
-    fun add _ (IConst _) =
-          I
-      | add vs (IVar v) =
-          if not (member (op =) vs v) then f v else I
-      | add vs (t1 `$ t2) =
-          add vs t1 #> add vs t2
-      | add vs ((v, _) `|-> t) =
-          add (insert (op =) v vs) t
-      | add vs (ICase ((td, _), bs)) =
-          add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs;
+    fun add _ (IConst _) = I
+      | add vs (IVar v) = if not (member (op =) vs v) then f v else I
+      | add vs (t1 `$ t2) = add vs t1 #> add vs t2
+      | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
+      | add vs (ICase (_, t)) = add vs t;
   in add [] end;
 
-fun collapse_let (((v, ty), se), be as ICase ((IVar w, _), ds)) =
+fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
       let
         fun exists_v t = fold_unbound_varnames (fn w => fn b =>
           b orelse v = w) t false;
       in if v = w andalso forall (fn (t1, t2) =>
         exists_v t1 orelse not (exists_v t2)) ds
-        then ICase ((se, ty), ds)
-        else ICase ((se, ty), [(IVar v, be)])
+        then ((se, ty), ds)
+        else ((se, ty), [(IVar v, be)])
       end
   | collapse_let (((v, ty), se), be) =
-      ICase ((se, ty), [(IVar v, be)])
+      ((se, ty), [(IVar v, be)])
 
 fun eta_expand (c as (_, (_, tys)), ts) k =
   let
diff -r 605f664d5115 -r 7b28dc69bdbb src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Pure/codegen.ML	Tue Aug 07 09:40:34 2007 +0200
@@ -377,7 +377,8 @@
     fn thm => add_unfold thm #> CodeData.add_inline thm));
   val _ = map (Context.add_setup o add_del_attribute) [
     ("func", (CodeData.add_func true, CodeData.del_func)),
-    ("inline", (CodeData.add_inline, CodeData.del_inline))
+    ("inline", (CodeData.add_inline, CodeData.del_inline)),
+    ("post", (CodeData.add_post, CodeData.del_post))
   ];
 end; (*local*)
 
diff -r 605f664d5115 -r 7b28dc69bdbb src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Aug 07 09:38:48 2007 +0200
+++ b/src/Tools/nbe.ML	Tue Aug 07 09:40:34 2007 +0200
@@ -351,7 +351,8 @@
   Logic.mk_equals (t, eval thy code t t');
 
 fun normalization_invoke thy code t t' =
-  Thm.invoke_oracle_i thy "Nbe.normalization" (thy, Normalization (code, t, t'));
+  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t'));
+  (*FIXME get rid of hardwired theory name "HOL"*)
 
 fun normalization_conv ct =
   let