certificates for code generator case expressions

--- a/src/HOL/Code_Setup.thy	Thu Oct 04 19:46:09 2007 +0200
+++ b/src/HOL/Code_Setup.thy	Thu Oct 04 19:54:44 2007 +0200
@@ -127,11 +127,6 @@
 
 lemmas [code func] = Let_def if_True if_False
 
-setup {*
-  CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let)
-  #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if)
-*}
-
 
 subsection {* Evaluation oracle *}
 
@@ -160,5 +155,4 @@
       THEN' resolve_tac [TrueI, refl]))
 *} "solve goal by normalization"
 
-
 end

--- a/src/HOL/HOL.thy	Thu Oct 04 19:46:09 2007 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 04 19:54:44 2007 +0200
@@ -1687,6 +1687,23 @@
 
 code_datatype "TYPE('a)"
 
+lemma Let_case_cert:
+  assumes "CASE \<equiv> (\<lambda>x. Let x f)"
+  shows "CASE x \<equiv> f x"
+  using assms by simp_all
+
+lemma If_case_cert:
+  includes meta_conjunction_syntax
+  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
+  shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
+  using assms by simp_all
+
+setup {*
+  Code.add_case @{thm Let_case_cert}
+  #> Code.add_case @{thm If_case_cert}
+  #> Code.add_undefined @{const_name undefined}
+*}
+
 
 subsection {* Legacy tactics and ML bindings *}
 

--- a/src/HOL/Product_Type.thy	Thu Oct 04 19:46:09 2007 +0200
+++ b/src/HOL/Product_Type.thy	Thu Oct 04 19:54:44 2007 +0200
@@ -807,12 +807,10 @@
 declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
 declare prod_caseE' [elim!] prod_caseE [elim!]
 
-lemma prod_case_split [code post]:
+lemma prod_case_split:
   "prod_case = split"
   by (auto simp add: expand_fun_eq)
 
-lemmas [code inline] = prod_case_split [symmetric]
-
 
 subsection {* Further cases/induct rules for tuples *}
 
@@ -902,6 +900,15 @@
 lemma [code func]:
   "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
 
+lemma split_case_cert:
+  assumes "CASE \<equiv> split f"
+  shows "CASE (a, b) \<equiv> f a b"
+  using assms by simp
+
+setup {*
+  Code.add_case @{thm split_case_cert}
+*}
+
 code_type *
   (SML infix 2 "*")
   (OCaml infix 2 "*")

--- a/src/Pure/Isar/code.ML	Thu Oct 04 19:46:09 2007 +0200
+++ b/src/Pure/Isar/code.ML	Thu Oct 04 19:54:44 2007 +0200
@@ -24,12 +24,16 @@
   val del_post: thm -> theory -> theory
   val add_datatype: (string * typ) list -> theory -> theory
   val add_datatype_cmd: string list -> theory -> theory
+  val add_case: thm -> theory -> theory
+  val add_undefined: string -> theory -> theory
 
   val coregular_algebra: theory -> Sorts.algebra
   val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
   val these_funcs: theory -> string -> thm list
   val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
   val get_datatype_of_constr: theory -> string -> string option
+  val get_case_data: theory -> string -> (int * string list) option
+  val is_undefined: theory -> string -> bool
   val default_typ: theory -> string -> typ
 
   val preprocess_conv: cterm -> thm
@@ -89,9 +93,9 @@
 fun certificate thy f r =
   case Susp.peek r
    of SOME thms => (Susp.value o f thy) thms
-     | NONE => let
-          val thy_ref = Theory.check_thy thy;
-        in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
+    | NONE => let
+        val thy_ref = Theory.check_thy thy;
+      in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
 
 fun merge' _ ([], []) = (false, [])
   | merge' _ ([], ys) = (true, ys)
@@ -231,10 +235,6 @@
     fun merge c x = let val (touched, thms') = merge_sdthms x in
       (if touched then cs''' := cons c (!cs''') else (); thms') end;
   in (cs'' @ !cs''', Symtab.join merge tabs) end;
-fun merge_funcs (thms1, thms2) =
-  let
-    val (consts, thms) = join_func_thms (thms1, thms2);
-  in (SOME consts, thms) end;
 
 val eq_string = op = : string * string -> bool;
 fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
@@ -253,22 +253,37 @@
       then raise Symtab.SAME else cos2;
   in ((new_types, diff_types), Symtab.join join tabs) end;
 
+fun merge_cases ((cases1, undefs1), (cases2, undefs2)) =
+  let
+    val touched1 = subtract (op =) (Symtab.keys cases1) (Symtab.keys cases2)
+      @ subtract (op =) (Symtab.keys cases2) (Symtab.keys cases1);
+    val touched2 = subtract (op =) (Symtab.keys undefs1) (Symtab.keys undefs2)
+      @ subtract (op =) (Symtab.keys undefs2) (Symtab.keys undefs1);
+    val touched = fold (insert (op =)) touched1 touched2;
+  in
+    (touched, (Symtab.merge (K true) (cases1, cases2),
+      Symtab.merge (K true) (undefs1, undefs2)))
+  end;
+
 datatype spec = Spec of {
   funcs: sdthms Symtab.table,
-  dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
+  dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
+  cases: (int * string list) Symtab.table * unit Symtab.table
 };
 
-fun mk_spec (funcs, dtyps) =
-  Spec { funcs = funcs, dtyps = dtyps };
-fun map_spec f (Spec { funcs = funcs, dtyps = dtyps }) =
-  mk_spec (f (funcs, dtyps));
-fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1 },
-  Spec { funcs = funcs2, dtyps = dtyps2 }) =
+fun mk_spec (funcs, (dtyps, cases)) =
+  Spec { funcs = funcs, dtyps = dtyps, cases = cases };
+fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
+  mk_spec (f (funcs, (dtyps, cases)));
+fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
+  Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
   let
-    val (touched_cs, funcs) = merge_funcs (funcs1, funcs2);
+    val (touched_cs, funcs) = join_func_thms (funcs1, funcs2);
     val ((new_types, diff_types), dtyps) = merge_dtyps (dtyps1, dtyps2);
-    val touched = if new_types orelse diff_types then NONE else touched_cs;
-  in (touched, mk_spec (funcs, dtyps)) end;
+    val (touched_cases, cases) = merge_cases (cases1, cases2);
+    val touched = if new_types orelse diff_types then NONE else
+      SOME (fold (insert (op =)) touched_cases touched_cs);
+  in (touched, mk_spec (funcs, (dtyps, cases))) end;
 
 datatype exec = Exec of {
   thmproc: thmproc,
@@ -287,15 +302,17 @@
     val touched = if touched' then NONE else touched_cs;
   in (touched, mk_exec (thmproc, spec)) end;
 val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
-  mk_spec (Symtab.empty, Symtab.empty));
+  mk_spec (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
 
 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 the_cases = #cases o the_spec;
 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;
+val map_dtyps = map_exec o apsnd o map_spec o apsnd o apfst;
+val map_cases = map_exec o apsnd o map_spec o apsnd o apsnd;
 
 
 (* data slots dependent on executable content *)
@@ -376,7 +393,7 @@
 
 (* access to executable content *)
 
-val get_exec = fst o CodeData.get;
+val the_exec = fst o CodeData.get;
 
 fun map_exec_purge touched f thy =
   CodeData.map (fn (exec, data) => 
@@ -413,7 +430,7 @@
 fun print_codesetup thy =
   let
     val ctxt = ProofContext.init thy;
-    val exec = get_exec thy;
+    val exec = the_exec thy;
     fun pretty_func (s, lthms) =
       (Pretty.block o Pretty.fbreaks) (
         Pretty.str s :: pretty_sdthms ctxt lthms
@@ -532,7 +549,7 @@
       o try (AxClass.params_of_class thy)) class;
     val funcs = classparams
       |> map (fn c => Class.inst_const thy (c, tyco))
-      |> map (Symtab.lookup ((the_funcs o get_exec) thy))
+      |> map (Symtab.lookup ((the_funcs o the_exec) thy))
       |> (map o Option.map) (Susp.force o fst)
       |> maps these
       |> map (Thm.transfer thy)
@@ -653,7 +670,7 @@
   else error ("No such " ^ msg ^ ": " ^ quote key);
 
 fun get_datatype thy tyco =
-  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
+  case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
    of SOME spec => spec
     | NONE => Sign.arity_number thy tyco
         |> Name.invents Name.context "'a"
@@ -663,7 +680,7 @@
 fun get_datatype_of_constr thy c =
   case (snd o strip_type o Sign.the_const_type thy) c
    of Type (tyco, _) => if member (op =)
-       ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o get_exec) thy)) tyco) c
+       ((the_default [] o Option.map (map fst o snd) o Symtab.lookup ((the_dtyps o the_exec) thy)) tyco) c
        then SOME tyco else NONE
     | _ => NONE;
 
@@ -676,6 +693,10 @@
         in SOME (Logic.varifyT ty) end
     | NONE => NONE;
 
+val get_case_data = Symtab.lookup o fst o the_cases o the_exec;
+
+val is_undefined = Symtab.defined o snd o the_cases o the_exec;
+
 fun add_func thm thy =
   let
     val func = mk_func thm;
@@ -746,7 +767,7 @@
     val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
     val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
     val purge_cs = map fst (snd vs_cos);
-    val purge_cs' = case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
+    val purge_cs' = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
      of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos)
       | NONE => NONE;
   in
@@ -760,6 +781,16 @@
     val cs = map (CodeUnit.read_bare_const thy) raw_cs;
   in add_datatype cs thy end;
 
+fun add_case thm thy =
+  let
+    val entry as (c, _) = CodeUnit.case_cert thm;
+  in
+    (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update entry) thy
+  end;
+
+fun add_undefined c thy =
+  (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
+
 fun add_inline thm thy =
   (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
     (insert Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
@@ -850,9 +881,9 @@
 
 fun preprocess thy thms =
   thms
-  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o get_exec) thy)
-  |> map (CodeUnit.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)
+  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o the_exec) thy)
+  |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o the_exec) thy))
+  |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy)
 (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
   |> common_typ_funcs
   |> map (Conv.fconv_rule (Class.unoverload thy));
@@ -862,9 +893,9 @@
     val thy = Thm.theory_of_cterm ct;
   in
     ct
-    |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o get_exec) thy)
+    |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy)
     |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
-        ((#inline_procs o the_thmproc o get_exec) thy)
+        ((#inline_procs o the_thmproc o the_exec) thy)
     |> rhs_conv (Class.unoverload thy)
   end;
 
@@ -876,7 +907,7 @@
   in
     ct
     |> Class.overload thy
-    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy))
+    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy))
   end;
 
 fun postprocess_term thy = term_of_conv thy postprocess_conv;
@@ -894,7 +925,7 @@
 local
 
 fun get_funcs thy const =
-  Symtab.lookup ((the_funcs o get_exec) thy) const
+  Symtab.lookup ((the_funcs o the_exec) thy) const
   |> Option.map (Susp.force o fst)
   |> these
   |> map (Thm.transfer thy);

--- a/src/Pure/Isar/code_unit.ML	Thu Oct 04 19:46:09 2007 +0200
+++ b/src/Pure/Isar/code_unit.ML	Thu Oct 04 19:54:44 2007 +0200
@@ -2,11 +2,23 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Basic units of code generation.  Auxiliary.
+Basic notions of code generation.  Auxiliary.
 *)
 
 signature CODE_UNIT =
 sig
+  (*generic non-sense*)
+  val bad_thm: string -> 'a
+  val error_thm: (thm -> thm) -> thm -> thm
+  val warning_thm: (thm -> thm) -> thm -> thm option
+  val try_thm: (thm -> thm) -> thm -> thm option
+
+  (*typ instantiations*)
+  val typ_sort_inst: Sorts.algebra -> typ * sort
+    -> sort Vartab.table -> sort Vartab.table
+  val inst_thm: sort Vartab.table -> thm -> thm
+
+  (*constants*)
   val string_of_typ: theory -> typ -> string
   val string_of_const: theory -> string -> string
   val no_args: theory -> string -> int
@@ -15,25 +27,22 @@
   val read_const_exprs: theory -> (string list -> string list)
     -> string list -> bool * string list
 
+  (*constructor sets*)
   val constrset_of_consts: theory -> (string * typ) list
     -> string * ((string * sort) list * (string * typ list) list)
-  val typ_sort_inst: Sorts.algebra -> typ * sort
-    -> sort Vartab.table -> sort Vartab.table
 
+  (*defining equations*)
   val assert_rew: thm -> thm
   val mk_rew: thm -> thm
   val mk_func: thm -> thm
   val head_func: thm -> string * typ
-  val bad_thm: string -> 'a
-  val error_thm: (thm -> thm) -> thm -> thm
-  val warning_thm: (thm -> thm) -> thm -> thm option
-  val try_thm: (thm -> thm) -> thm -> thm option
-
-  val inst_thm: sort Vartab.table -> thm -> thm
   val expand_eta: int -> thm -> thm
   val rewrite_func: thm list -> thm -> thm
   val norm_args: thm list -> thm list 
-  val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list 
+  val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list
+
+  (*case certificates*)
+  val case_cert: thm -> string * (int * string list)
 end;
 
 structure CodeUnit: CODE_UNIT =
@@ -360,4 +369,49 @@
     |> map Drule.zero_var_indexes
   end;
 
+
+(* case cerificates *)
+
+fun case_cert thm =
+  let
+    (*FIXME rework this code*)
+    val thy = Thm.theory_of_thm thm;
+    val (cas, t_pats) = (Logic.dest_implies o Thm.prop_of) thm;
+    val pats = Logic.dest_conjunctions t_pats;
+    val (head, proto_case_expr) = Logic.dest_equals cas;
+    val _ = case head of Free _ => true
+      | Var _ => true
+      | _ => raise TERM ("case_cert", []);
+    val ([(case_expr_v, _)], case_expr) = Term.strip_abs_eta 1 proto_case_expr;
+    val (Const (c_case, _), raw_params) = strip_comb case_expr;
+    val i = find_index
+      (fn Free (v, _) => v = case_expr_v | _ => false) raw_params;
+    val _ = if i = ~1 then raise TERM ("case_cert", []) else ();
+    val t_params = nth_drop i raw_params;
+    val params = map (fst o dest_Var) t_params;
+    fun dest_pat t =
+      let
+        val (head' $ t_co, rhs) = Logic.dest_equals t;
+        val _ = if head' = head then () else raise TERM ("case_cert", []);
+        val (Const (co, _), args) = strip_comb t_co;
+        val (Var (param, _), args') = strip_comb rhs;
+        val _ = if args' = args then () else raise TERM ("case_cert", []);
+      in (param, co) end;
+    fun analyze_pats pats =
+      let
+        val co_list = fold (AList.update (op =) o dest_pat) pats [];
+      in map (the o AList.lookup (op =) co_list) params end;
+    fun analyze_let t =
+      let
+        val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t;
+        val _ = if head' = head then () else raise TERM ("case_cert", []);
+        val _ = if arg' = arg then () else raise TERM ("case_cert", []);
+        val _ = if [param'] = params then () else raise TERM ("case_cert", []);
+      in [] end;
+  in (c_case, (i, case pats
+   of [pat] => (analyze_pats pats handle Bind => analyze_let pat)
+    | _ :: _ => analyze_pats pats))
+  end handle Bind => error "bad case certificate"
+    | TERM _ => error "bad case certificate";
+
 end;

--- a/src/Tools/code/code_package.ML	Thu Oct 04 19:46:09 2007 +0200
+++ b/src/Tools/code/code_package.ML	Thu Oct 04 19:54:44 2007 +0200
@@ -20,14 +20,6 @@
   val eval_invoke: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
     -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
   val codegen_command: theory -> string -> unit;
-
-  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;
 end;
 
 structure CodePackage : CODE_PACKAGE =
@@ -35,23 +27,7 @@
 
 open BasicCodeThingol;
 
-(** code translation **)
-
-(* theory data *)
-
-type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
-  -> CodeFuncgr.T
-  -> (string * typ) * term list -> CodeThingol.transact -> iterm * CodeThingol.transact;
-
-structure Appgens = TheoryDataFun
-(
-  type T = (int * (appgen * stamp)) Symtab.table;
-  val empty = Symtab.empty;
-  val copy = I;
-  val extend = I;
-  fun merge _ = Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
-    bounds1 = bounds2 andalso stamp1 = stamp2);
-);
+(** code theorems **)
 
 fun code_depgr thy [] = CodeFuncgr.make thy []
   | code_depgr thy consts =
@@ -80,6 +56,9 @@
     val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
   in Present.display_graph prgr end;
 
+
+(** code translation **)
+
 structure Program = CodeDataFun
 (
   type T = CodeThingol.code;
@@ -313,29 +292,55 @@
   exprgen_const thy algbr funcgr c_ty
   ##>> fold_map (exprgen_term thy algbr funcgr) ts
   #>> (fn (t, ts) => t `$$ ts)
-and exprgen_app thy algbr funcgr ((c, ty), ts) =
-  case Symtab.lookup (Appgens.get thy) c
-   of SOME (i, (appgen, _)) =>
-        if length ts < i then
-          let
-            val k = length ts;
-            val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
-            val ctxt = (fold o fold_aterms)
-              (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
-            val vs = Name.names ctxt "a" tys;
-          in
-            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
-        else if length ts > i then
-          appgen thy algbr funcgr ((c, ty), Library.take (i, ts))
-          ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
-          #>> (fn (t, ts) => t `$$ ts)
-        else
-          appgen thy algbr funcgr ((c, ty), ts)
-    | NONE =>
-        exprgen_app_default thy algbr funcgr ((c, ty), ts);
+and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
+  let
+    (*FIXME rework this code*)
+    val (all_tys, _) = strip_type ty;
+    val (tys, _) = chop (1 + (if null cases then 1 else length cases)) all_tys;
+    val st = nth ts n;
+    val sty = nth tys n;
+    fun is_undefined (Const (c, _)) = Code.is_undefined thy c
+      | is_undefined _ = false;
+    fun mk_case (co, n) t =
+      let
+        val (vs, body) = Term.strip_abs_eta n t;
+        val selector = list_comb (Const (co, map snd vs ---> sty), map Free vs);
+      in if is_undefined body then NONE else SOME (selector, body) end;
+    val ds = case cases
+     of [] => let val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
+          in [(Free v_ty, body)] end
+      | cases => map_filter (uncurry mk_case) (AList.make (CodeUnit.no_args thy) cases
+          ~~ nth_drop n ts);
+  in
+    exprgen_term thy algbr funcgr st
+    ##>> exprgen_typ thy algbr funcgr sty
+    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
+          ##>> exprgen_term thy algbr funcgr body) ds
+    ##>> exprgen_app_default thy algbr funcgr app
+    #>> (fn (((st, sty), ds), t0) => ICase (((st, sty), ds), t0))
+  end
+and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
+ of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
+      if length ts < i then
+        let
+          val k = length ts;
+          val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
+          val ctxt = (fold o fold_aterms)
+            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
+          val vs = Name.names ctxt "a" tys;
+        in
+          fold_map (exprgen_typ thy algbr funcgr) tys
+          ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
+          #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
+        end
+      else if length ts > i then
+        exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
+        ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
+        #>> (fn (t, ts) => t `$$ ts)
+      else
+        exprgen_case thy algbr funcgr n cases ((c, ty), ts)
+      end
+  | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
 
 
 (* entrance points into translation kernel *)
@@ -362,52 +367,6 @@
     ^ CodeUnit.string_of_typ thy ty_decl);
 
 
-(* 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)) =
-  let
-    val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
-    fun clause_gen (dt, bt) =
-      exprgen_term thy algbr funcgr
-        (map_aterms (fn Const (c_ty as (c, ty)) => Const
-          (Class.unoverload_const thy c_ty, ty) | t => t) dt)
-      ##>> exprgen_term thy algbr funcgr bt;
-  in
-    exprgen_term thy algbr funcgr st
-    ##>> exprgen_typ thy algbr funcgr sty
-    ##>> fold_map clause_gen ds
-    ##>> exprgen_app_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])) =
-  exprgen_term thy algbr funcgr ct
-  ##>> exprgen_term thy algbr funcgr st
-  ##>> exprgen_app_default thy algbr funcgr app
-  #>> (fn (((v, ty) `|-> be, se), t0) =>
-            ICase (CodeThingol.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
-  ##>> exprgen_app_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
-    val i = (length o fst o strip_type o Sign.the_const_type thy) c;
-    val _ = Program.change thy (K CodeThingol.empty_code);
-  in
-    Appgens.map (Symtab.update (c, (i, (appgen, stamp ())))) thy
-  end;
-
-
 (** code generation interfaces **)
 
 (* generic generation combinators *)