# HG changeset patch
# User haftmann
# Date 1152716422 -7200
# Node ID 454f4be984b7963f596c061bca2a7796312efab4
# Parent  f8e7c71926e4bca1f025c0f21dee430860bb3f43
adaptions in codegen

diff -r f8e7c71926e4 -r 454f4be984b7 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/Datatype.thy	Wed Jul 12 17:00:22 2006 +0200
@@ -227,9 +227,9 @@
   "is_none None = True"
   "is_none (Some x) = False"
 
-lemma is_none_none [code unfolt]:
+lemma is_none_none [code inline]:
   "(x = None) = (is_none x)" 
-by (cases "x") simp_all
+by (cases x) simp_all
 
 lemmas [code] = imp_conv_disj
 
@@ -257,6 +257,10 @@
   fst_conv [code]
   snd_conv [code]
 
+lemma split_is_prod_case [code inline]:
+  "split = prod_case"
+by (simp add: expand_fun_eq split_def prod.cases)
+
 code_typapp bool
   ml (target_atom "bool")
   haskell (target_atom "Bool")
diff -r f8e7c71926e4 -r 454f4be984b7 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Jul 12 17:00:22 2006 +0200
@@ -888,7 +888,7 @@
 lemma [code]: "nat i = nat_aux 0 i"
   by (simp add: nat_aux_def)
 
-lemma [code unfolt]:
+lemma [code inline]:
   "neg k = (k < 0)"
   unfolding neg_def ..
 
@@ -959,9 +959,7 @@
 
 setup {*
   Codegen.add_codegen "number_of_codegen" number_of_codegen
-  #> CodegenPackage.add_appconst
-       ("Numeral.number_of", ((1, 1),
-          appgen_number))
+  (* #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number) *)
   #> CodegenPackage.set_int_tyco "IntDef.int"
 *}
 
diff -r f8e7c71926e4 -r 454f4be984b7 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed Jul 12 17:00:22 2006 +0200
@@ -781,23 +781,23 @@
 
 subsection {* code generator setup *}
 
-lemma elim_nat [code unfolt]:
+lemma elim_nat [code inline]:
   "(number_of n :: nat) = nat (number_of n)"
   by simp
 
-lemma elim_zero [code unfolt]:
+lemma elim_zero [code inline]:
   "(0::int) = number_of (Numeral.Pls)" 
   by simp
 
-lemma elim_one [code unfolt]:
+lemma elim_one [code inline]:
   "(1::int) = number_of (Numeral.Pls BIT bit.B1)" 
   by simp
 
-lemma elim_one_nat [code unfolt]:
+lemma elim_one_nat [code inline]:
   "1 = Suc 0"
   by simp
 
-lemmas [code unfolt] =
+lemmas [code inline] =
   bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
   bin_pred_Pls  bin_pred_Min  bin_pred_1  bin_pred_0
 
diff -r f8e7c71926e4 -r 454f4be984b7 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Wed Jul 12 17:00:22 2006 +0200
@@ -77,7 +77,7 @@
   by unfolding in place.
 *}
 
-lemma [code unfolt]:
+lemma [code inline]:
   "0 = nat 0"
   "Suc = (op +) 1"
 by (simp_all add: expand_fun_eq)
diff -r f8e7c71926e4 -r 454f4be984b7 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/List.thy	Wed Jul 12 17:00:22 2006 +0200
@@ -270,7 +270,7 @@
 lemma null_empty: "null xs = (xs = [])"
   by (cases xs) simp_all
 
-lemma empty_null [code unfolt]:
+lemma empty_null [code inline]:
   "(xs = []) = null xs"
 using null_empty [symmetric] .
 
@@ -2698,12 +2698,13 @@
 val list_codegen_setup =
   Codegen.add_codegen "list_codegen" list_codegen
   #> Codegen.add_codegen "char_codegen" char_codegen
+  #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number)
   #> fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
        ("ml", (7, "::")),
        ("haskell", (5, ":"))
      ]
   #> CodegenPackage.add_appconst
-       ("List.char.Char", ((2, 2), CodegenPackage.appgen_char dest_char));
+       ("List.char.Char", CodegenPackage.appgen_char dest_char);
 
 end;
 *}
diff -r f8e7c71926e4 -r 454f4be984b7 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/Product_Type.thy	Wed Jul 12 17:00:22 2006 +0200
@@ -842,12 +842,10 @@
   | _ => NONE);
 
 val prod_codegen_setup =
-  Codegen.add_codegen "let_codegen" let_codegen #>
-  Codegen.add_codegen "split_codegen" split_codegen #>
-  CodegenPackage.add_appconst
-    ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs_split)) #>
-  CodegenPackage.add_appconst
-    ("split", ((1, 1), CodegenPackage.appgen_split strip_abs_split));
+  Codegen.add_codegen "let_codegen" let_codegen
+  #> Codegen.add_codegen "split_codegen" split_codegen
+  #> CodegenPackage.add_appconst
+       ("Let", CodegenPackage.appgen_let)
 
 *}
 
diff -r f8e7c71926e4 -r 454f4be984b7 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/datatype_codegen.ML
     ID:         $Id$
-    Author:     Stefan Berghofer, TU Muenchen
+    Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
 
 Code generator for inductive datatypes.
 *)
@@ -10,6 +10,8 @@
   val get_datatype_spec_thms: theory -> string
     -> (((string * sort) list * (string * typ list) list) * tactic) option
   val get_all_datatype_cons: theory -> (string * string) list
+  val dest_case_expr: theory -> term
+    -> ((string * typ) list * ((term * typ) * (term * term) list)) option;
   val add_datatype_case_const: string -> theory -> theory
   val add_datatype_case_defs: string -> theory -> theory
   val setup: theory -> theory
@@ -304,6 +306,34 @@
 
 (** code 2nd generation **)
 
+fun dtyp_of_case_const thy c =
+  get_first (fn (dtco, { case_name, ... }) => if case_name = c then SOME dtco else NONE)
+    ((Symtab.dest o DatatypePackage.get_datatypes) thy);
+
+fun dest_case_app cs ts tys =
+  let
+    val abs = CodegenThingol.give_names [] (Library.drop (length ts, tys));
+    val (ts', t) = split_last (ts @ map Free abs);
+    val (tys', sty) = split_last tys;
+    fun freenames_of t = fold_aterms
+      (fn Free (v, _) => insert (op =) v | _ => I) t [];
+    fun dest_case ((c, tys_decl), ty) t =
+      let
+        val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
+        val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
+      in (c', t') end;
+  in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts')) end;
+
+fun dest_case_expr thy t =
+  case strip_comb t
+   of (Const (c, ty), ts) =>
+        (case dtyp_of_case_const thy c
+         of SOME dtco =>
+              let val (vs, cs) = (the o DatatypePackage.get_datatype_spec thy) dtco;
+              in SOME (dest_case_app cs ts (Library.take (length cs + 1, (fst o strip_type) ty))) end
+          | _ => NONE)
+    | _ => NONE;
+
 fun datatype_tac thy dtco =
   let
     val ctxt = Context.init_proof thy;
@@ -333,10 +363,9 @@
 
 fun add_datatype_case_const dtco thy =
   let
-    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco
+    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
   in
-    CodegenPackage.add_case_const case_name
-      ((map (apsnd length) o #3 o the o AList.lookup (op =) descr) index) thy
+    CodegenPackage.add_appconst_i (case_name, CodegenPackage.appgen_case dest_case_expr) thy
   end;
 
 fun add_datatype_case_defs dtco thy =
@@ -351,8 +380,6 @@
   add_tycodegen "datatype" datatype_tycodegen #>
   CodegenTheorems.add_datatype_extr
     get_datatype_spec_thms #>
-  CodegenPackage.set_get_datatype
-    DatatypePackage.get_datatype_spec #>
   CodegenPackage.set_get_all_datatype_cons
     get_all_datatype_cons #>
   DatatypeHooks.add add_datatype_case_const #>
diff -r f8e7c71926e4 -r 454f4be984b7 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Wed Jul 12 17:00:22 2006 +0200
@@ -292,7 +292,7 @@
 *}
 
 setup {*
-  CodegenPackage.add_appconst ("wfrec", ((3, 3), CodegenPackage.appgen_wfrec))
+  CodegenPackage.add_appconst ("wfrec", CodegenPackage.appgen_wfrec)
 *}
 
 code_constapp
diff -r f8e7c71926e4 -r 454f4be984b7 src/Pure/Tools/ROOT.ML
--- a/src/Pure/Tools/ROOT.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/Pure/Tools/ROOT.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -11,13 +11,11 @@
 (*code generator, 1st generation*)
 use "../codegen.ML";
 
-(*code generator theorems*)
-use "codegen_theorems.ML";
-use "codegen_simtype.ML";
-
 (*code generator, 2nd generation*)
 use "codegen_thingol.ML";
 use "codegen_serializer.ML";
+use "codegen_theorems.ML";
+use "codegen_simtype.ML";
 use "codegen_package.ML";
 
 (*Steven Obua's evaluator*)
diff -r f8e7c71926e4 -r 454f4be984b7 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -8,7 +8,7 @@
 
 signature CODEGEN_PACKAGE =
 sig
-  val codegen_term: term -> theory -> CodegenThingol.iexpr * theory;
+  val codegen_term: term -> theory -> CodegenThingol.iterm * theory;
   val is_dtcon: string -> bool;
   val consts_of_idfs: theory -> string list -> (string * typ) list;
   val idfs_of_consts: theory -> (string * typ) list -> string list;
@@ -22,22 +22,19 @@
   val add_alias: string * string -> theory -> theory;
   val set_get_all_datatype_cons : (theory -> (string * string) list)
     -> theory -> theory;
-  val set_get_datatype: (theory -> string -> ((string * sort) list * (string * typ list) list) option)
-    -> theory -> theory;
   val set_int_tyco: string -> theory -> theory;
 
   type appgen;
-  val add_appconst: xstring * ((int * int) * appgen) -> theory -> theory;
-  val add_appconst_i: string * ((int * int) * appgen) -> theory -> theory;
+  val add_appconst: xstring * appgen -> theory -> theory;
+  val add_appconst_i: string * appgen -> theory -> theory;
   val appgen_default: appgen;
-  val appgen_let: (int -> term -> term list * term)
-    -> appgen;
-  val appgen_split: (int -> term -> term list * term)
-    -> appgen;
   val appgen_number_of: (theory -> term -> IntInf.int) -> appgen;
   val appgen_char: (term -> int option) -> appgen;
+  val appgen_case: (theory -> term
+    -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
+    -> appgen;
+  val appgen_let: appgen;
   val appgen_wfrec: appgen;
-  val add_case_const: string -> (string * int) list -> theory -> theory;
 
   val print_code: theory -> unit;
   val rename_inconsistent: theory -> theory;
@@ -240,7 +237,7 @@
 type eqextr_default = theory -> auxtab
   -> string * typ -> ((thm list * term option) * typ) option;
 type appgen = theory -> auxtab
-  -> (string * typ) * term list -> transact -> iexpr * transact;
+  -> (string * typ) * term list -> transact -> iterm * transact;
 
 val serializers = ref (
   Symtab.empty
@@ -268,51 +265,33 @@
   | merge_opt eq (SOME x1, SOME x2) =
       if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
 
-type gens = {
-  appconst: ((int * int) * (appgen * stamp)) Symtab.table,
-  eqextrs: (string * (eqextr_default * stamp)) list
-};
+type appgens = (int * (appgen * stamp)) Symtab.table
 
-fun map_gens f { appconst, eqextrs } =
-  let
-    val (appconst, eqextrs) =
-      f (appconst, eqextrs)
-  in { appconst = appconst, eqextrs = eqextrs } : gens end;
-
-fun merge_gens
-  ({ appconst = appconst1 , eqextrs = eqextrs1 },
-   { appconst = appconst2 , eqextrs = eqextrs2 }) =
-  { appconst = Symtab.merge
-      (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2
-         andalso stamp1 = stamp2)
-      (appconst1, appconst2),
-    eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2)
-  } : gens;
+fun merge_appgens x =
+  Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
+    bounds1 = bounds2 andalso stamp1 = stamp2) x
 
 type logic_data = {
   get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option,
-  get_datatype: ((theory -> string -> ((string * sort) list * (string * typ list) list) option) * stamp) option,
   alias: string Symtab.table * string Symtab.table
 };
 
-fun map_logic_data f { get_all_datatype_cons, get_datatype, alias } =
+fun map_logic_data f { get_all_datatype_cons, alias } =
   let
-    val ((get_all_datatype_cons, get_datatype), alias) =
-      f ((get_all_datatype_cons, get_datatype), alias)
+    val (get_all_datatype_cons, alias) =
+      f (get_all_datatype_cons, alias)
   in { get_all_datatype_cons = get_all_datatype_cons,
-    get_datatype = get_datatype, alias = alias } : logic_data end;
+    alias = alias } : logic_data end;
 
 fun merge_logic_data
   ({ get_all_datatype_cons = get_all_datatype_cons1,
-       get_datatype = get_datatype1, alias = alias1 },
+       alias = alias1 },
    { get_all_datatype_cons = get_all_datatype_cons2,
-       get_datatype = get_datatype2, alias = alias2 }) =
+       alias = alias2 }) =
   let
   in
     { get_all_datatype_cons = merge_opt (eq_snd (op =))
         (get_all_datatype_cons1, get_all_datatype_cons2),
-      get_datatype = merge_opt (eq_snd (op =))
-        (get_datatype1, get_datatype2),
       alias = (Symtab.merge (op =) (fst alias1, fst alias2),
                Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data
   end;
@@ -320,7 +299,7 @@
 type target_data = {
   syntax_class: string Symtab.table,
   syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table,
-  syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table
+  syntax_const: (iterm CodegenSerializer.pretty_syntax * stamp) Symtab.table
 };
 
 fun map_target_data f { syntax_class, syntax_tyco, syntax_const } =
@@ -345,15 +324,14 @@
   val name = "Pure/codegen_package";
   type T = {
     modl: module,
-    gens: gens,
+    appgens: appgens,
     logic_data: logic_data,
     target_data: target_data Symtab.table
   };
   val empty = {
     modl = empty_module,
-    gens = { appconst = Symtab.empty, eqextrs = [] } : gens,
+    appgens = Symtab.empty,
     logic_data = { get_all_datatype_cons = NONE,
-      get_datatype = NONE,
       alias = (Symtab.empty, Symtab.empty) } : logic_data,
     target_data =
       Symtab.empty
@@ -365,13 +343,13 @@
   val copy = I;
   val extend = I;
   fun merge _ (
-    { modl = modl1, gens = gens1,
+    { modl = modl1, appgens = appgens1,
       target_data = target_data1, logic_data = logic_data1 },
-    { modl = modl2, gens = gens2,
+    { modl = modl2, appgens = appgens2,
       target_data = target_data2, logic_data = logic_data2 }
   ) = {
     modl = merge_module (modl1, modl2),
-    gens = merge_gens (gens1, gens2),
+    appgens = merge_appgens (appgens1, appgens2),
     logic_data = merge_logic_data (logic_data1, logic_data2),
     target_data = Symtab.join (K merge_target_data) (target_data1, target_data2)
   };
@@ -387,10 +365,10 @@
 
 fun map_codegen_data f thy =
   case CodegenData.get thy
-   of { modl, gens, target_data, logic_data } =>
-      let val (modl, gens, target_data, logic_data) =
-        f (modl, gens, target_data, logic_data)
-      in CodegenData.put { modl = modl, gens = gens,
+   of { modl, appgens, target_data, logic_data } =>
+      let val (modl, appgens, target_data, logic_data) =
+        f (modl, appgens, target_data, logic_data)
+      in CodegenData.put { modl = modl, appgens = appgens,
            target_data = target_data, logic_data = logic_data } thy end;
 
 val print_code = CodegenData.print;
@@ -450,7 +428,7 @@
    of SOME idf => idf
     | NONE => case get_overloaded (c, ty)
    of SOME idf => idf
-    | NONE => case AxClass.class_of thy c
+    | NONE => case AxClass.class_of_param thy c
    of SOME _ => idf_of_name thy nsp_mem c
     | NONE => idf_of_name thy nsp_const c
   end;
@@ -468,7 +446,7 @@
         | _ => NONE)
   in case get_overloaded (c, ty)
    of SOME idf => idf
-    | NONE => case AxClass.class_of thy c
+    | NONE => case AxClass.class_of_param thy c
    of SOME _ => idf_of_name thy nsp_mem c
     | NONE => idf_of_name thy nsp_const c
   end;
@@ -488,17 +466,17 @@
 
 (* further theory data accessors *)
 
-fun gen_add_appconst prep_const (raw_c, (bounds, ag)) thy =
+fun gen_add_appconst prep_const (raw_c, appgen) thy =
   let
     val c = prep_const thy raw_c;
+    val _ = writeln c;
+    val i = (length o fst o strip_type o Sign.the_const_type thy) c
+    val _ = (writeln o string_of_int) i;
   in map_codegen_data
-    (fn (modl, gens, target_data, logic_data) =>
+    (fn (modl, appgens, target_data, logic_data) =>
        (modl,
-        gens |> map_gens
-          (fn (appconst, eqextrs) =>
-            (appconst
-             |> Symtab.update (c, (bounds, (ag, stamp ()))),
-             eqextrs)), target_data, logic_data)) thy
+        appgens |> Symtab.update (c, (i, (appgen, stamp ()))),
+        target_data, logic_data)) thy
   end;
 
 val add_appconst = gen_add_appconst Sign.intern_const;
@@ -509,27 +487,13 @@
     (fn (modl, gens, target_data, logic_data) =>
        (modl, gens, target_data,
         logic_data
-        |> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype)
-             => (SOME (f, stamp ()), get_datatype))))));
+        |> map_logic_data (apfst (fn _ => SOME (f, stamp ())))));
 
 fun get_all_datatype_cons thy =
   case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy
    of NONE => []
     | SOME (f, _) => f thy;
 
-fun set_get_datatype f =
-  map_codegen_data
-    (fn (modl, gens, target_data, logic_data) =>
-       (modl, gens, target_data,
-        logic_data
-        |> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype)
-             => (get_all_datatype_cons, SOME (f, stamp ())))))));
-
-fun get_datatype thy =
-  case (#get_datatype o #logic_data o CodegenData.get) thy
-   of NONE => K NONE
-    | SOME (f, _) => f thy;
-
 fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf =
   case recconst_of_idf thy tabs idf
    of SOME c_ty => SOME c_ty
@@ -678,10 +642,14 @@
             trns
             |> fold_map (exprgen_term thy tabs) args
             ||>> exprgen_term thy tabs rhs;
+          fun checkvars (args, rhs) =
+            if CodegenThingol.vars_distinct args then (args, rhs)
+            else error ("repeated variables on left hand side of function")
         in
           trns
           |> message msg (fn trns => trns
           |> fold_map (exprgen_eq o dest_eqthm) eq_thms
+          |-> (fn eqs => pair (map checkvars eqs))
           ||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext
           ||>> exprgen_type thy tabs ty
           |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), map snd sortcontext)))
@@ -760,7 +728,7 @@
        of SOME m =>
             trns
             |> debug_msg (fn _ => "trying defgen class member for " ^ quote m)
-            |> ensure_def_class thy tabs ((the o AxClass.class_of thy) m)
+            |> ensure_def_class thy tabs ((the o AxClass.class_of_param thy) m)
             |-> (fn cls => succeed Bot)
         | _ =>
             trns |> fail ("no class member found for " ^ quote m)
@@ -803,7 +771,7 @@
       |-> (fn ty => pair (IVar v))
   | exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
       let
-        val (v, t) = Term.variant_abs (CodegenTheorems.proper_name raw_v, ty, raw_t);
+        val (v, t) = Term.variant_abs (CodegenThingol.proper_name raw_v, ty, raw_t);
       in
         trns
         |> exprgen_type thy tabs ty
@@ -834,23 +802,22 @@
   |-> (fn (((c, ty), ls), es) =>
          pair (IConst (c, (ls, ty)) `$$ es))
 and appgen thy tabs ((f, ty), ts) trns =
-  case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
-   of SOME ((imin, imax), (ag, _)) =>
-        if length ts < imin then
+  case Symtab.lookup ((#appgens o CodegenData.get) thy) f
+   of SOME (i, (ag, _)) =>
+        if length ts < i then
           let
-            val d = imin - length ts;
-            val vs = Name.invent_list (add_term_names (Const (f, ty), [])) "x" d;
-            val tys = Library.take (d, ((fst o strip_type) ty));
+            val tys = Library.take (i - length ts, ((fst o strip_type) ty));
+            val vs = CodegenThingol.give_names [f] tys;
           in
             trns
             |> fold_map (exprgen_type thy tabs) tys
-            ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys)
-            |-> (fn (tys, e) => pair (vs ~~ tys `|--> e))
+            ||>> ag thy tabs ((f, ty), ts @ map Free vs)
+            |-> (fn (tys, e) => pair (map2 (fn (v, _) => pair v) vs tys `|--> e))
           end
-        else if length ts > imax then
+        else if length ts > i then
           trns
-          |> ag thy tabs ((f, ty), Library.take (imax, ts))
-          ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts))
+          |> ag thy tabs ((f, ty), Library.take (i, ts))
+          ||>> fold_map (exprgen_term thy tabs) (Library.drop (i, ts))
           |-> (fn (e, es) => pair (e `$$ es))
         else
           trns
@@ -862,33 +829,6 @@
 
 (* parametrized generators, for instantiation in HOL *)
 
-fun appgen_split strip_abs thy tabs (app as (c_ty, [t])) trns =
-  case strip_abs 1 (Const c_ty $ t)
-   of ([vt], bt) =>
-        trns
-        |> exprgen_term thy tabs vt
-        ||>> exprgen_type thy tabs (type_of vt)
-        ||>> exprgen_term thy tabs bt
-        ||>> appgen_default thy tabs app
-        |-> (fn (((ve, vty), be), e0) => pair (IAbs (((ve, vty), be), e0)))
-    | _ =>
-        trns
-        |> appgen_default thy tabs app;
-
-fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
-  case strip_abs 1 ct
-   of ([st], bt) =>
-        trns
-        |> exprgen_term thy tabs dt
-        ||>> exprgen_type thy tabs (type_of dt)
-        ||>> exprgen_term thy tabs st
-        ||>> exprgen_term thy tabs bt
-        ||>> appgen_default thy tabs app
-        |-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0)))
-    | _ =>
-        trns
-        |> appgen_default thy tabs app;
-
 fun appgen_number_of int_of_bin thy tabs (app as (c as (_, ty), [bin])) trns =
   case try (int_of_bin thy) bin
    of SOME i => if i < 0 then error ("negative numeral: " ^ IntInf.toString i)
@@ -914,6 +854,36 @@
         trns
         |> appgen_default thy tabs app;
 
+fun appgen_case dest_case_expr thy tabs (app as (c_ty, ts)) trns =
+  let
+    val _ = (writeln o fst) c_ty;
+    val _ = (writeln o Sign.string_of_typ thy o snd) c_ty;
+    val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
+    fun clausegen (dt, bt) trns =
+      trns
+      |> exprgen_term thy tabs dt
+      ||>> exprgen_term thy tabs bt;
+  in
+    trns
+    |> exprgen_term thy tabs st
+    ||>> exprgen_type thy tabs sty
+    ||>> fold_map clausegen ds
+    ||>> appgen_default thy tabs app
+    |-> (fn (((se, sty), ds), e0) => pair (ICase (((se, sty), ds), e0)))
+  end;
+
+fun appgen_let thy tabs (app as (_, [st, ct])) trns =
+  trns
+  |> exprgen_term thy tabs ct
+  ||>> exprgen_term thy tabs st
+  ||>> appgen_default thy tabs app
+  |-> (fn (((v, ty) `|-> be, se), e0) =>
+            pair (ICase (((se, ty), case be
+              of ICase (((IVar w, _), ds), _) => if v = w then ds else [(IVar v, be)]
+               | _ => [(IVar v, be)]
+            ), e0))
+        | (_, e0) => pair e0);
+
 fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
   let
     val ty_def = (op ---> o apfst tl o strip_type o Logic.legacy_unvarifyT o Sign.the_const_type thy) c;
@@ -931,42 +901,6 @@
     |-> (fn ((((_, ls), ty), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
   end;
 
-fun appgen_datatype_case cos thy tabs (app as ((_, ty), ts)) trns =
-  let
-    val (ts', t) = split_last ts;
-    val (tys, dty) = (split_last o fst o strip_type) ty;
-    fun gen_names i =
-      Name.invent_list (foldr add_term_names
-       (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts) "xa" i;
-    fun cg_case_d (((cname, i), ty), t) trns =
-      let
-        val vs = gen_names i;
-        val tys = Library.take (i, (fst o strip_type) ty);
-        val frees = map2 (curry Free) vs tys;
-        val t' = Envir.beta_norm (list_comb (t, frees));
-      in
-        trns
-        |> exprgen_term thy tabs (list_comb (Const (cname, tys ---> dty), frees))
-        ||>> exprgen_term thy tabs t'
-        |-> (fn (ep, e) => pair (ep, e))
-      end;
-  in
-    trns
-    |> exprgen_term thy tabs t
-    ||>> exprgen_type thy tabs dty
-    ||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts')
-    ||>> appgen_default thy tabs app
-    |-> (fn (((de, dty), bses), e0) => pair (ICase (((de, dty), bses), e0)))
-  end;
-
-fun add_case_const c cos thy =
-  let
-    val n_eta = length cos + 1;
-  in
-    thy
-    |> add_appconst_i (c, ((n_eta, n_eta), appgen_datatype_case cos))
-  end;
-
 
 
 (** theory interface **)
@@ -998,7 +932,7 @@
           (fn (c, _) =>
             let
               val deftab = Theory.definitions_of thy c
-              val is_overl = (is_none o AxClass.class_of thy) c
+              val is_overl = (is_none o AxClass.class_of_param thy) c
                andalso case deftab   (* is_overloaded (!?) *)
                of [] => false
                 | [{lhs = ty, ...}] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
@@ -1102,8 +1036,9 @@
       else add_alias (src, dst) thy
   in fold add inconsistent thy end;
 
-fun codegen_term t =
-  expand_module NONE NONE exprgen_term t;
+fun codegen_term t thy =
+  thy
+  |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) NONE exprgen_term t;
 
 val is_dtcon = has_nsp nsp_dtcon;
 
diff -r f8e7c71926e4 -r 454f4be984b7 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -14,13 +14,13 @@
       -> OuterParse.token list ->
       ((string -> string option)
         * (string -> CodegenThingol.itype pretty_syntax option)
-        * (string -> CodegenThingol.iexpr pretty_syntax option)
+        * (string -> CodegenThingol.iterm pretty_syntax option)
       -> string list * string list option
       -> CodegenThingol.module -> unit)
       * OuterParse.token list;
   val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
     ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
-  val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax;
+  val pretty_list: string -> string -> int * string -> CodegenThingol.iterm pretty_syntax;
   val serializers: {
     ml: string * (string * string * (string -> bool) -> serializer),
     haskell: string * (string * string list -> serializer)
@@ -28,7 +28,7 @@
   val mk_flat_ml_resolver: string list -> string -> string;
   val ml_fun_datatype: string * string * (string -> bool)
     -> ((string -> CodegenThingol.itype pretty_syntax option)
-        * (string -> CodegenThingol.iexpr pretty_syntax option))
+        * (string -> CodegenThingol.iterm pretty_syntax option))
     -> (string -> string)
     -> ((string * CodegenThingol.funn) list -> Pretty.T)
         * ((string * CodegenThingol.datatyp) list -> Pretty.T);
@@ -198,7 +198,7 @@
     -> OuterParse.token list ->
     ((string -> string option)
       * (string -> itype pretty_syntax option)
-      * (string -> iexpr pretty_syntax option)
+      * (string -> iterm pretty_syntax option)
     -> string list * string list option
     -> CodegenThingol.module -> unit)
     * OuterParse.token list;
@@ -289,6 +289,12 @@
           | _ => SOME)
        | _ => Scan.fail ());
 
+fun parse_stdout serializer =
+  OuterParse.name
+  >> (fn "_" => serializer
+        (fn "" => (fn p => (Pretty.writeln p; NONE))
+          | _ => SOME)
+       | _ => Scan.fail ());
 
 (* list serializer *)
 
@@ -329,9 +335,9 @@
   type src = string;
   val ord = string_ord;
   fun mk reserved_ml (name, 0) =
-        (CodegenTheorems.proper_name o NameSpace.base) name
+        (CodegenThingol.proper_name o NameSpace.base) name
     | mk reserved_ml (name, i) =
-        (CodegenTheorems.proper_name o NameSpace.base) name ^ replicate_string i "'";
+        (CodegenThingol.proper_name o NameSpace.base) name ^ replicate_string i "'";
   fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
   fun maybe_unique _ _ = NONE;
   fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
@@ -458,13 +464,15 @@
                   ml_from_expr NOBR e1,
                   ml_from_expr BR e2
                 ])
-      | ml_from_expr fxy ((v, ty) `|-> e) =
-          brackify BR [
-            str "fn",
-            typify ty (str v),
-            str "=>",
-            ml_from_expr NOBR e
-          ]
+      | ml_from_expr fxy (e as _ `|-> _) =
+          let
+            val (es, be) = CodegenThingol.unfold_abs e;
+            fun mk_abs (e, ty) = (Pretty.block o Pretty.breaks) [
+                str "fn",
+                typify ty (ml_from_expr NOBR e),
+                str "=>"
+              ];
+          in brackify BR (map mk_abs es @ [ml_from_expr NOBR be]) end
       | ml_from_expr fxy (INum (n, _)) =
           brackify BR [
             (str o IntInf.toString) n,
@@ -475,16 +483,9 @@
           (str o prefix "#" o quote)
             (let val i = (Char.ord o the o Char.fromString) c
               in if i < 32 
-                then prefix "\\" c
+                then prefix "\\" (string_of_int i)
                 else c
               end)
-      | ml_from_expr fxy (IAbs (((ve, vty), be), _)) =
-          brackify BR [
-            str "fn",
-            typify vty (ml_from_expr NOBR ve),
-            str "=>",
-            ml_from_expr NOBR be
-          ]
       | ml_from_expr fxy (e as ICase ((_, [_]), _)) =
           let
             val (ves, be) = CodegenThingol.unfold_let e;
@@ -519,7 +520,7 @@
             @ [str ")"]
           ) end
       | ml_from_expr _ e =
-          error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iexpr) e)
+          error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
     and ml_mk_app f es =
       if is_cons f andalso length es > 1 then
         [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
@@ -553,7 +554,6 @@
           let
             fun no_eta (_::_, _) = I
               | no_eta (_, _ `|-> _) = I
-              | no_eta (_, IAbs (_, _)) = I
               | no_eta ([], e) = K false;
             fun has_tyvars (_ `%% tys) =
                   exists has_tyvars tys
@@ -816,6 +816,7 @@
   in
     parse_multi
     || parse_internal serializer
+    || parse_stdout serializer
     || parse_single_file serializer
   end;
 
@@ -910,20 +911,9 @@
           (str o enclose "'" "'")
             (let val i = (Char.ord o the o Char.fromString) c
               in if i < 32 
-                then Library.prefix "\\" c
+                then Library.prefix "\\" (string_of_int i)
                 else c
               end)
-      | hs_from_expr fxy (e as IAbs _) =
-          let
-            val (es, e) = CodegenThingol.unfold_abs e
-          in
-            brackify BR (
-              str "\\"
-              :: map (hs_from_expr BR o fst) es @ [
-              str "->",
-              hs_from_expr NOBR e
-            ])
-          end
       | hs_from_expr fxy (e as ICase ((_, [_]), _)) =
           let
             val (ps, body) = CodegenThingol.unfold_let e;
diff -r f8e7c71926e4 -r 454f4be984b7 src/Pure/Tools/codegen_simtype.ML
--- a/src/Pure/Tools/codegen_simtype.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/Pure/Tools/codegen_simtype.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -29,7 +29,7 @@
           else raise TYPE ("dest_fun", [ty], [])
       | dest_fun ty = raise TYPE ("dest_fun", [ty], []);
     val PROP = ObjectLogic.ensure_propT thy
-    val (ty_abs, ty_rep) = (dest_fun o type_of) repm;
+    val (ty_abs, ty_rep) = (dest_fun o fastype_of) repm;
     val (tyco_abs, ty_parms) = dest_Type ty_abs;
     val _ = if exists (fn TFree _ => false | _ => true) ty_parms then raise TYPE ("no TFree", ty_parms, []) else ();
     val repv = Free ("x", ty_rep);
diff -r f8e7c71926e4 -r 454f4be984b7 src/Pure/Tools/codegen_theorems.ML
--- a/src/Pure/Tools/codegen_theorems.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -20,7 +20,6 @@
   val purge_defs: string * typ -> theory -> theory;
   val notify_dirty: theory -> theory;
 
-  val proper_name: string -> string;
   val extr_typ: theory -> thm -> typ;
   val common_typ: theory -> (thm -> typ) -> thm list -> thm list;
   val preprocess: theory -> thm list -> thm list;
@@ -58,29 +57,6 @@
 
 (* auxiliary *)
 
-fun proper_name s =
-  let
-    fun replace_invalid c =
-      if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
-        andalso not (NameSpace.separator = c)
-      then c
-      else "_";
-    fun contract "_" (acc as "_" :: _) = acc
-      | contract c acc = c :: acc;
-    fun contract_underscores s =
-      implode (fold_rev contract (explode s) []);
-    fun ensure_char s =
-      if forall (Char.isDigit o the o Char.fromString) (explode s)
-        then prefix "x" s
-        else s
-  in
-    s
-    |> translate_string replace_invalid
-    |> contract_underscores
-    |> ensure_char
-  end;
-
-
 fun getf_first [] _ = NONE
   | getf_first (f::fs) x = case f x
      of NONE => getf_first fs x
@@ -190,7 +166,7 @@
 fun mk_obj_eq thy (x, y) =
   let
     val ((b, _), ((tr, fl), (con, eq))) = get_obj thy;
-  in Const (eq, type_of x --> type_of y --> b) $ x $ y end;
+  in Const (eq, fastype_of x --> fastype_of y --> b) $ x $ y end;
 
 fun is_obj_eq thy c =
   let
@@ -214,7 +190,7 @@
     fun expvars t =
       let
         val lhs = (fst o Logic.dest_equals) t;
-        val tys = (fst o strip_type o type_of) lhs;
+        val tys = (fst o strip_type o fastype_of) lhs;
         val used = fold_aterms (fn Var ((v, _), _) => insert (op =) v | _ => I) lhs [];
         val vs = Name.invent_list used "x" (length tys);
       in
@@ -248,7 +224,7 @@
             (ctyp_of thy ty, ctyp_of thy (TVar ((v', maxidx), sort))) :: acc)
         end;
     val lower_name = (prefix "'" o implode o map (Char.toString o Char.toLower o the o Char.fromString)
-      o explode o proper_name o unprefix "'");
+      o explode o CodegenThingol.proper_name o unprefix "'");
     fun tvars_of thm = (fold_types o fold_atyps)
       (fn TVar (v_i as (v, i), sort) => cons (v_i, (lower_name v, sort))
         | _ => I) (prop_of thm) [];
@@ -267,7 +243,7 @@
             (cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc)
         end;
     val lower_name = (implode o map (Char.toString o Char.toLower o the o Char.fromString)
-      o explode o proper_name);
+      o explode o CodegenThingol.proper_name);
     fun vars_of thm = fold_aterms
       (fn Var (v_i as (v, i), ty) => cons (v_i, (lower_name v, ty))
         | _ => I) (prop_of thm) [];
@@ -577,7 +553,7 @@
         fun incr_thm thm max =
           let
             val thm' = incr_indexes max thm;
-            val max' = (maxidx_of_typ o type_of o Drule.plain_prop_of) thm' + 1;
+            val max' = (maxidx_of_typ o fastype_of o Drule.plain_prop_of) thm' + 1;
           in (thm', max') end;
         val (thms', maxidx) = fold_map incr_thm thms 0;
         val (ty1::tys) = map extract_typ thms;
@@ -765,7 +741,7 @@
   val _ = map (Context.add_setup o add_simple_attribute) [
     ("fun", add_fun),
     ("unfold", (fn thm => Codegen.add_unfold thm #> add_unfold thm)),
-    ("unfolt", add_unfold),
+    ("inline", add_unfold),
     ("nofold", del_unfold)
   ]
 end; (*local*)
diff -r f8e7c71926e4 -r 454f4be984b7 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -24,17 +24,14 @@
       `%% of string * itype list
     | `-> of itype * itype
     | ITyVar of vname;
-  datatype iexpr =
+  datatype iterm =
       IConst of string * (iclasslookup list list * itype)
     | IVar of vname
-    | `$ of iexpr * iexpr
-    | `|-> of (vname * itype) * iexpr
-    | INum of IntInf.int (*non-negative!*) * iexpr
-    | IChar of string (*length one!*) * iexpr
-    | IAbs of ((iexpr * itype) * iexpr) * iexpr
-        (* (((binding expression (ve), binding type (vty)),
-                body expression (be)), native expression (e0)) *)
-    | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
+    | `$ of iterm * iterm
+    | `|-> of (vname * itype) * iterm
+    | INum of IntInf.int (*non-negative!*) * iterm
+    | IChar of string (*length one!*) * iterm
+    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
         (* ((discrimendum expression (de), discrimendum type (dty)),
                 [(selector expression (se), body expression (be))]),
                 native expression (e0)) *)
@@ -44,27 +41,31 @@
 sig
   include BASIC_CODEGEN_THINGOL;
   val `--> : itype list * itype -> itype;
-  val `$$ : iexpr * iexpr list -> iexpr;
-  val `|--> : (vname * itype) list * iexpr -> iexpr;
+  val `$$ : iterm * iterm list -> iterm;
+  val `|--> : (vname * itype) list * iterm -> iterm;
   val pretty_itype: itype -> Pretty.T;
-  val pretty_iexpr: iexpr -> Pretty.T;
+  val pretty_iterm: iterm -> Pretty.T;
   val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
   val unfold_fun: itype -> itype list * itype;
-  val unfold_app: iexpr -> iexpr * iexpr list;
-  val unfold_abs: iexpr -> (iexpr * itype) list * iexpr;
-  val unfold_let: iexpr -> ((iexpr * itype) * iexpr) list * iexpr;
-  val unfold_const_app: iexpr ->
-    ((string * (iclasslookup list list * itype)) * iexpr list) option;
-  val add_constnames: iexpr -> string list -> string list;
-  val add_varnames: iexpr -> string list -> string list;
-  val is_pat: (string -> bool) -> iexpr -> bool;
-  val map_pure: (iexpr -> 'a) -> iexpr -> 'a;
-  val resolve_tycos: (string -> string) -> itype * iexpr list -> itype * iexpr list;
-  val resolve_consts: (string -> string) -> iexpr -> iexpr;
-  val eta_expand: (string * (iclasslookup list list * itype)) * iexpr list -> int -> iexpr;
+  val unfold_app: iterm -> iterm * iterm list;
+  val unfold_abs: iterm -> (iterm * itype) list * iterm;
+  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
+  val unfold_const_app: iterm ->
+    ((string * (iclasslookup list list * itype)) * iterm list) option;
+  val add_constnames: iterm -> string list -> string list;
+  val add_varnames: iterm -> string list -> string list;
+  val is_pat: (string -> bool) -> iterm -> bool;
+  val vars_distinct: iterm list -> bool;
+  val map_pure: (iterm -> 'a) -> iterm -> 'a;
+  val eta_expand: (string * (iclasslookup list list * itype)) * iterm list -> int -> iterm;
+  val proper_name: string -> string;
+  val invent_name: string list -> string;
+  val give_names: string list -> 'a list -> (string * 'a) list;
+  val resolve_tycos: (string -> string) -> itype * iterm list -> itype * iterm list;
+  val resolve_consts: (string -> string) -> iterm -> iterm;
 
-  type funn = (iexpr list * iexpr) list * (sortcontext * itype);
+  type funn = (iterm list * iterm) list * (sortcontext * itype);
   type datatyp = sortcontext * (string * itype list) list;
   datatype def =
       Bot
@@ -131,20 +132,27 @@
     | SOME (x1, x2) =>
         let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
 
-fun map_yield f [] = ([], [])
-  | map_yield f (x::xs) =
-      let
-        val (y, x') = f x
-        val (ys, xs') = map_yield f xs
-      in (y::ys, x'::xs') end;
-
-fun get_prefix eq ([], ys) = ([], ([], ys))
-  | get_prefix eq (xs, []) = ([], (xs, []))
-  | get_prefix eq (xs as x::xs', ys as y::ys') =
-      if eq (x, y) then
-        let val (ps', xys'') = get_prefix eq (xs', ys')
-        in (x::ps', xys'') end
-      else ([], (xs, ys));
+fun proper_name s =
+  let
+    fun replace_invalid c =
+      if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
+        andalso not (NameSpace.separator = c)
+      then c
+      else "_";
+    fun contract "_" (acc as "_" :: _) = acc
+      | contract c acc = c :: acc;
+    fun contract_underscores s =
+      implode (fold_rev contract (explode s) []);
+    fun ensure_char s =
+      if forall (Char.isDigit o the o Char.fromString) (explode s)
+        then prefix "x" s
+        else s
+  in
+    s
+    |> translate_string replace_invalid
+    |> contract_underscores
+    |> ensure_char
+  end;
 
 
 (** language core - types, pattern, expressions **)
@@ -163,15 +171,14 @@
   | `-> of itype * itype
   | ITyVar of vname;
 
-datatype iexpr =
+datatype iterm =
     IConst of string * (iclasslookup list list * itype)
   | IVar of vname
-  | `$ of iexpr * iexpr
-  | `|-> of (vname * itype) * iexpr
-  | INum of IntInf.int (*non-negative!*) * iexpr
-  | IChar of string (*length one!*) * iexpr
-  | IAbs of ((iexpr * itype) * iexpr) * iexpr
-  | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
+  | `$ of iterm * iterm
+  | `|-> of (vname * itype) * iterm
+  | INum of IntInf.int * iterm
+  | IChar of string * iterm
+  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
     (*see also signature*)
 
 (*
@@ -213,32 +220,29 @@
   | pretty_itype (ITyVar v) =
       Pretty.str v;
 
-fun pretty_iexpr (IConst (c, _)) =
+fun pretty_iterm (IConst (c, _)) =
       Pretty.str c
-  | pretty_iexpr (IVar v) =
+  | pretty_iterm (IVar v) =
       Pretty.str ("?" ^ v)
-  | pretty_iexpr (e1 `$ e2) =
-      (Pretty.enclose "(" ")" o Pretty.breaks)
-        [pretty_iexpr e1, pretty_iexpr e2]
-  | pretty_iexpr ((v, ty) `|-> e) =
+  | pretty_iterm (e1 `$ e2) =
       (Pretty.enclose "(" ")" o Pretty.breaks)
-        [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iexpr e]
-  | pretty_iexpr (INum (n, _)) =
+        [pretty_iterm e1, pretty_iterm e2]
+  | pretty_iterm ((v, ty) `|-> e) =
+      (Pretty.enclose "(" ")" o Pretty.breaks)
+        [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm e]
+  | pretty_iterm (INum (n, _)) =
       (Pretty.str o IntInf.toString) n
-  | pretty_iexpr (IChar (c, _)) =
+  | pretty_iterm (IChar (c, _)) =
       (Pretty.str o quote) c
-  | pretty_iexpr (IAbs (((e1, _), e2), _)) =
-      (Pretty.enclose "(" ")" o Pretty.breaks)
-        [pretty_iexpr e1, Pretty.str "|->", pretty_iexpr e2]
-  | pretty_iexpr (ICase (((e, _), cs), _)) =
+  | pretty_iterm (ICase (((e, _), cs), _)) =
       (Pretty.enclose "(" ")" o Pretty.breaks) [
         Pretty.str "case",
-        pretty_iexpr e,
+        pretty_iterm e,
         Pretty.enclose "(" ")" (map (fn (p, e) =>
           (Pretty.block o Pretty.breaks) [
-            pretty_iexpr p,
+            pretty_iterm p,
             Pretty.str "=>",
-            pretty_iexpr e
+            pretty_iterm e
           ]
         ) cs)
       ];
@@ -252,8 +256,9 @@
     | _ => NONE);
 
 val unfold_abs = unfoldr
-  (fn (v, ty) `|-> e => SOME ((IVar v, ty), e)
-    | IAbs (((e1, ty), e2), _) => SOME ((e1, ty), e2)
+  (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(se, be)]), _)) => 
+        if v = w then SOME ((se, ty), be) else SOME ((IVar v, ty), e)
+    | (v, ty) `|-> e => SOME ((IVar v, ty), e)
     | _ => NONE)
 
 val unfold_let = unfoldr
@@ -326,8 +331,6 @@
       error ("sorry, no pure representation for numerals so far")
   | map_pure f (IChar (_, e0)) =
       f e0
-  | map_pure f (IAbs (_, e0)) =
-      f e0
   | map_pure f (ICase (_, e0)) =
       f e0;
 
@@ -346,8 +349,6 @@
       I
   | add_constnames (IChar _) =
       I
-  | add_constnames (IAbs (_, e)) =
-      add_constnames e
   | add_constnames (ICase (_, e)) =
       add_constnames e;
 
@@ -363,23 +364,41 @@
       I
   | add_varnames (IChar _) =
       I
-  | add_varnames (IAbs (((ve, _), be), _)) =
-      add_varnames ve #> add_varnames be
   | add_varnames (ICase (((de, _), bses), _)) =
       add_varnames de #> fold (fn (be, se) => add_varnames be #> add_varnames se) bses;
 
-fun invent seed used =
+fun vars_distinct es =
   let
-    val x = Name.variant used seed
-  in (x, x :: used) end;
+    fun distinct _ NONE =
+          NONE
+      | distinct (IConst _) x =
+          x
+      | distinct (IVar v) (SOME vs) =
+          if member (op =) vs v then NONE else SOME (v::vs)
+      | distinct (e1 `$ e2) x =
+          x |> distinct e1 |> distinct e2
+      | distinct (_ `|-> e) x =
+          x |> distinct e
+      | distinct (INum _) x =
+          x
+      | distinct (IChar _) x =
+          x
+      | distinct (ICase (((de, _), bses), _)) x =
+          x |> distinct de |> fold (fn (be, se) => distinct be #> distinct se) bses;
+  in is_some (fold distinct es (SOME [])) end;
+
+fun invent_name used = hd (Name.invent_list used "a" 1);
+
+fun give_names used xs =
+  Name.invent_list used "a" (length xs) ~~ xs;
 
 fun eta_expand (c as (_, (_, ty)), es) k =
   let
     val j = length es;
     val l = k - j;
     val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty;
-    val vs = [] |> fold add_varnames es |> fold_map invent (replicate l "x") |> fst;
-  in vs ~~ tys `|--> IConst c `$$ es @ map IVar vs end;
+    val vs_tys = give_names (fold add_varnames es []) tys;
+  in vs_tys `|--> IConst c `$$ es @ map (fn (v, _) => IVar v) vs_tys end;
 
 
 
@@ -387,7 +406,7 @@
 
 (* type definitions *)
 
-type funn = (iexpr list * iexpr) list * (sortcontext * itype);
+type funn = (iterm list * iterm) list * (sortcontext * itype);
 type datatyp = sortcontext * (string * itype list) list;
 
 datatype def =
@@ -419,10 +438,10 @@
       Pretty.enum " |" "" "" (
         map (fn (ps, body) =>
           Pretty.block [
-            Pretty.enum "," "[" "]" (map pretty_iexpr ps),
+            Pretty.enum "," "[" "]" (map pretty_iterm ps),
             Pretty.str " |->",
             Pretty.brk 1,
-            pretty_iexpr body,
+            pretty_iterm body,
             Pretty.str "::",
             pretty_sortcontext sortctxt,
             Pretty.str "/",
@@ -615,8 +634,8 @@
     let
       val m1 = dest_name name1 |> apsnd single |> (op @);
       val m2 = dest_name name2 |> apsnd single |> (op @);
-      val (ms, (r1, r2)) = get_prefix (op =) (m1, m2);
-      val (ms, (s1::r1, s2::r2)) = get_prefix (op =) (m1, m2);
+      val (ms, (r1, r2)) = chop_prefix (op =) (m1, m2);
+      val (ms, (s1::r1, s2::r2)) = chop_prefix (op =) (m1, m2);
       val add_edge =
         if null r1 andalso null r2
         then Graph.add_edge
@@ -979,7 +998,7 @@
           in (p' :: ps', tab'') end;
     fun deresolv tab prefix name =
       let
-        val (common, (_, rem)) = get_prefix (op =) (prefix, NameSpace.unpack name);
+        val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name);
         val (_, SOME tab') = get_path_name common tab;
         val (name', _) = get_path_name rem tab';
       in NameSpace.pack name' end;
diff -r f8e7c71926e4 -r 454f4be984b7 src/Pure/Tools/nbe_eval.ML
--- a/src/Pure/Tools/nbe_eval.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/Pure/Tools/nbe_eval.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -25,7 +25,7 @@
     | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm)
                                          (*functions*);
 
-  val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm
+  val nbe: Univ Symtab.table -> CodegenThingol.iterm -> nterm
   val apply: Univ -> Univ -> Univ
 
   val to_term: Univ -> nterm