introduced characters for code generator; some improved code lemmas for some list functions

--- a/src/HOL/HOL.thy	Tue May 09 11:00:32 2006 +0200
+++ b/src/HOL/HOL.thy	Tue May 09 14:18:40 2006 +0200
@@ -1410,8 +1410,5 @@
   "op =" (* an intermediate solution for polymorphic equality *)
     ml (infixl 6 "=")
     haskell (infixl 4 "==")
-  arbitrary
-    ml ("raise/ (Fail/ \"non-defined-result\")")
-    haskell ("error/ \"non-defined result\"")
 
 end

--- a/src/HOL/List.thy	Tue May 09 11:00:32 2006 +0200
+++ b/src/HOL/List.thy	Tue May 09 14:18:40 2006 +0200
@@ -265,6 +265,12 @@
 by (rule measure_induct [of length]) iprover
 
 
+subsubsection {* @{text null} *}
+
+lemma null_empty: "null xs = (xs = [])"
+  by (cases xs) simp_all
+
+
 subsubsection {* @{text length} *}
 
 text {*
@@ -1080,6 +1086,18 @@
 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
 by(induct xs)(auto simp:neq_Nil_conv)
 
+lemma last_code [code]:
+  "last (x # xs) = (if null xs then x else last xs)"
+by (cases xs) simp_all
+
+declare last.simps [code del]
+
+lemma butlast_code [code]:
+  "butlast [] = []"
+  "butlast (x # xs) = (if null xs then [] else x # butlast xs)"
+by (simp, cases xs) simp_all
+
+declare butlast.simps [code del]
 
 subsubsection {* @{text take} and @{text drop} *}
 
@@ -1441,17 +1459,23 @@
 
 lemma list_all2_lengthD [intro?]: 
   "list_all2 P xs ys ==> length xs = length ys"
-by (simp add: list_all2_def)
-
-lemma list_all2_Nil [iff,code]: "list_all2 P [] ys = (ys = [])"
-by (simp add: list_all2_def)
-
-lemma list_all2_Nil2[iff]: "list_all2 P xs [] = (xs = [])"
-by (simp add: list_all2_def)
-
-lemma list_all2_Cons [iff,code]:
-"list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
-by (auto simp add: list_all2_def)
+  by (simp add: list_all2_def)
+
+lemma list_all2_Nil [iff]: "list_all2 P [] ys = (ys = [])"
+  by (simp add: list_all2_def)
+
+lemma list_all2_Nil2 [iff]: "list_all2 P xs [] = (xs = [])"
+  by (simp add: list_all2_def)
+
+lemma list_all2_Nil_code [code]: "list_all2 P [] ys = null ys"
+  unfolding null_empty by simp
+
+lemma list_all2_Nil2_code [code]: "list_all2 P xs [] = null xs"
+  unfolding null_empty by simp
+
+lemma list_all2_Cons [iff, code]:
+  "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
+  by (auto simp add: list_all2_def)
 
 lemma list_all2_Cons1:
 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
@@ -2174,15 +2198,15 @@
 
 subsubsection {* @{const splice} *}
 
-lemma splice_Nil2[simp]:
+lemma splice_Nil2 [simp, code]:
  "splice xs [] = xs"
 by (cases xs) simp_all
 
-lemma splice_Cons_Cons[simp]:
+lemma splice_Cons_Cons [simp, code]:
  "splice (x#xs) (y#ys) = x # y # splice xs ys"
 by simp
 
-declare splice.simps(2)[simp del]
+declare splice.simps(2) [simp del, code del]
 
 subsubsection{*Sets of Lists*}
 
@@ -2666,24 +2690,35 @@
     (gr, HOLogic.dest_list t)
   in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
 
-fun dest_nibble (Const (s, _)) = int_of_nibble (unprefix "List.nibble.Nibble" s)
-  | dest_nibble _ = raise Match;
-
-fun char_codegen thy defs gr dep thyname b (Const ("List.char.Char", _) $ c1 $ c2) =
-    (let val c = chr (dest_nibble c1 * 16 + dest_nibble c2)
-     in if Symbol.is_printable c then SOME (gr, Pretty.quote (Pretty.str c))
-       else NONE
-     end handle Fail _ => NONE | Match => NONE)
-  | char_codegen thy defs gr dep thyname b _ = NONE;
+fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
+      let
+        fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s
+          | dest_nibble _ = raise Match;
+      in
+        (SOME (dest_nibble c1 * 16 + dest_nibble c2)
+        handle Fail _ => NONE | Match => NONE)
+      end
+  | dest_char _ = NONE;
+
+fun char_codegen thy defs gr dep thyname b t =
+  case (Option.map chr o dest_char) t 
+   of SOME c =>
+        if Symbol.is_printable c
+        then SOME (gr, (Pretty.quote o Pretty.str) c)
+        else NONE
+    | NONE => NONE;
 
 in
 
 val list_codegen_setup =
-  Codegen.add_codegen "list_codegen" list_codegen #>
-  Codegen.add_codegen "char_codegen" char_codegen #>
-  fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
-    ("ml", (7, "::")),
-    ("haskell", (5, ":"))];
+  Codegen.add_codegen "list_codegen" list_codegen
+  #> Codegen.add_codegen "char_codegen" char_codegen
+  #> fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
+       ("ml", (7, "::")),
+       ("haskell", (5, ":"))
+     ]
+  #> CodegenPackage.add_appconst
+       ("List.char.Char", ((2, 2), CodegenPackage.appgen_char dest_char));
 
 end;
 *}
@@ -2729,6 +2764,11 @@
     ml (target_atom "[]")
     haskell (target_atom "[]")
 
+code_syntax_tyco
+  char
+    ml (target_atom "char")
+    haskell (target_atom "Char")
+
 setup list_codegen_setup
 
 setup CodegenPackage.rename_inconsistent

--- a/src/HOL/Main.thy	Tue May 09 11:00:32 2006 +0200
+++ b/src/HOL/Main.thy	Tue May 09 14:18:40 2006 +0200
@@ -11,8 +11,6 @@
 text {*
   Theory @{text Main} includes everything.  Note that theory @{text
   PreList} already includes most HOL theories.
-*}
-
 
 text {* \medskip Late clause setup: installs \emph{all} simprules and
   claset rules into the clause cache; cf.\ theory @{text

--- a/src/Pure/Tools/codegen_package.ML	Tue May 09 11:00:32 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Tue May 09 14:18:40 2006 +0200
@@ -47,6 +47,7 @@
   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_wfrec: appgen;
   val add_case_const: string -> (string * int) list -> theory -> theory;
 
@@ -827,9 +828,20 @@
   in
     trns
     |> exprgen_type thy tabs ty
-    |-> (fn ty => pair (CodegenThingol.INum ((i, ty), ())))
+    |-> (fn _ => pair (CodegenThingol.INum (i, ())))
   end;
 
+fun appgen_char char_to_index thy tabs (app as ((_, ty), _)) trns =
+  case (char_to_index o list_comb o apfst Const) app
+   of SOME i =>
+        trns
+        |> exprgen_type thy tabs ty
+        ||>> appgen_default thy tabs app
+        |-> (fn (_, e0) => pair (IChar (chr i, e0)))
+    | NONE =>
+        trns
+        |> appgen_default thy tabs app;
+
 fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
   let
     val ty_def = (op ---> o apfst tl o strip_type o Type.unvarifyT o Sign.the_const_type thy) c;

--- a/src/Pure/Tools/codegen_serializer.ML	Tue May 09 11:00:32 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue May 09 14:18:40 2006 +0200
@@ -86,20 +86,14 @@
 fun brackify_infix infx fxy_ctxt ps =
   gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
 
-fun from_app mk_app from_expr const_syntax fxy ((c, ty), es) =
-  let
-    fun mk NONE es =
-          brackify fxy (mk_app c es)
-      | mk (SOME ((i, k), pr)) es =
-          (*if i <= length es then*)
-            let
-              val (es1, es2) = chop k es;
-            in
-              brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
-            end
-          (*else
-            error ("illegal const_syntax")*)
-  in mk (const_syntax c) es end;
+fun from_app mk_app from_expr const_syntax fxy (const as (c, _), es) =
+  case (const_syntax c)
+   of NONE => brackify fxy (mk_app c es)
+    | SOME ((i, k), pr) =>
+        if i <= length es
+          then case chop k es of (es1, es2) =>
+            brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
+          else from_expr fxy (CodegenThingol.eta_expand (const, es) i);
 
 fun fillin_mixfix fxy_this ms fxy_ctxt pr args =
   let
@@ -218,7 +212,7 @@
     | (p, ss) => error ("Malformed definition: " ^ quote s ^ " - " ^ commas ss);
 
 
-(* abstract serializer *)
+(* generic abstract serializer *)
 
 type serializer = 
     string list list
@@ -231,7 +225,7 @@
     * OuterParse.token list;
 
 fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
-    postprocess preprocess (class_syntax, tyco_syntax, const_syntax)
+    postprocess (class_syntax, tyco_syntax, const_syntax)
     select module =
   let
     fun pretty_of_prim resolv (name, primdef) =
@@ -251,8 +245,6 @@
     module
     |> debug_msg (fn _ => "selecting submodule...")
     |> (if is_some select then (CodegenThingol.project_module o the) select else I)
-    |> debug_msg (fn _ => "preprocessing...")
-    |> preprocess
     |> debug_msg (fn _ => "serializing...")
     |> CodegenThingol.serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
          from_module' validator postproc nspgrp name_root
@@ -371,7 +363,7 @@
         (CodegenTheorems.proper_name o NameSpace.base) name
     | mk reserved_ml (name, i) =
         (CodegenTheorems.proper_name o NameSpace.base) name ^ replicate_string i "'";
-  fun is_valid reserved_ml = not o member (op = : string * string -> bool) reserved_ml;
+  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);
 );
@@ -499,12 +491,18 @@
             str "=>",
             ml_from_expr NOBR e
           ]
-      | ml_from_expr fxy (INum ((n, ty), _)) =
+      | ml_from_expr fxy (INum (n, _)) =
           brackify BR [
             (str o IntInf.toString) n,
-            str ":",
-            ml_from_type NOBR ty
+            str ":IntInf.int"
           ]
+      | ml_from_expr _ (IChar (c, _)) =
+          (str o prefix "#" o quote)
+            (let val i = (Char.ord o the o Char.fromString) c
+              in if i < 32 
+                then prefix "\\" c
+                else c
+              end)
       | ml_from_expr fxy (IAbs (((ve, vty), be), _)) =
           brackify BR [
             str "fn",
@@ -552,10 +550,10 @@
         [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
       else
         (str o resolv) f :: map (ml_from_expr BR) es
-    and ml_from_app fxy ((c, (lss, ty)), es) =
+    and ml_from_app fxy (app_expr as ((c, (lss, ty)), es)) =
       case map (ml_from_sortlookup BR) lss
        of [] =>
-            from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
+            from_app ml_mk_app ml_from_expr const_syntax fxy app_expr
         | lss =>
             brackify fxy (
               (str o resolv) c
@@ -574,6 +572,24 @@
       in
         Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
       end;
+    fun eta_expand_poly_fun (funn as (_, (_::_, _))) =
+          funn
+      | eta_expand_poly_fun (funn as (eqs, sctxt_ty as (_, ty))) =
+          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
+              | has_tyvars (ITyVar _) =
+                  true
+              | has_tyvars (ty1 `-> ty2) =
+                  has_tyvars ty1 orelse has_tyvars ty2;
+          in if (not o has_tyvars) ty orelse fold no_eta eqs true
+            then funn
+            else (map (fn ([], rhs) => ([IVar "x"], rhs `$ IVar "x")) eqs, sctxt_ty)
+          end;
     fun ml_from_funs (defs as def::defs_tl) =
       let
         fun mk_definer [] [] = "val"
@@ -608,10 +624,11 @@
               :: map (mk_eq "|") eq_tl
             )
           end;
+        val def' :: defs' = map (apsnd eta_expand_poly_fun o constructive_fun) defs
       in
         chunk_defs (
-          (mk_fun (the (fold check_args defs NONE)) o constructive_fun) def
-          :: map (mk_fun "and" o constructive_fun) defs_tl
+          (mk_fun (the (fold check_args defs NONE))) def'
+          :: map (mk_fun "and") defs'
         )
       end;
     fun ml_from_datatypes (defs as (def::defs_tl)) =
@@ -818,14 +835,6 @@
                   let val l = AList.lookup (op =) cs s |> the |> length
                   in if l >= 2 then l else 0 end
                 else 0;
-    fun preprocess const_syntax module =
-      module
-      |> debug_msg (fn _ => "eta-expanding...")
-      |> CodegenThingol.eta_expand (eta_expander module const_syntax)
-      |> debug_msg (fn _ => "eta-expanding polydefs...")
-      |> CodegenThingol.eta_expand_poly
-      (*|> debug 3 (fn _ => "unclashing expression/type variables...")
-      |> CodegenThingol.unclash_vars_tvars*);
     val parse_multi =
       OuterParse.name
       #-> (fn "dir" => 
@@ -838,7 +847,7 @@
      || parse_internal serializer
      || parse_single_file serializer)
     >> (fn seri => fn (class_syntax, tyco_syntax, const_syntax) => seri 
-         (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax))
+         (class_syntax, tyco_syntax, const_syntax))
   end;
 
 fun mk_flat_ml_resolver names =
@@ -926,13 +935,15 @@
               hs_from_expr NOBR e
             ])
           end
-      | hs_from_expr fxy (INum ((n, ty), _)) =
-          brackify BR [
-            (str o (fn s => if nth_string s 0 = "~"
-              then enclose "(" ")" ("negate " ^ unprefix "~" s) else s) o IntInf.toString) n,
-            str "::",
-            hs_from_type NOBR ty
-          ]
+      | hs_from_expr fxy (INum (n, _)) =
+          (str o IntInf.toString) n
+      | hs_from_expr fxy (IChar (c, _)) =
+          (str o enclose "'" "'")
+            (let val i = (Char.ord o the o Char.fromString) c
+              in if i < 32 
+                then Library.prefix "\\" c
+                else c
+              end)
       | hs_from_expr fxy (e as IAbs _) =
           let
             val (es, e) = CodegenThingol.unfold_abs e
@@ -975,8 +986,8 @@
           ] end
     and hs_mk_app c es =
       (str o resolv) c :: map (hs_from_expr BR) es
-    and hs_from_app fxy ((c, (ty, ls)), es) =
-      from_app hs_mk_app hs_from_expr const_syntax fxy ((c, ty), es);
+    and hs_from_app fxy =
+      from_app hs_mk_app hs_from_expr const_syntax fxy
     fun hs_from_funeqs (def as (name, _)) =
       let
         fun from_eq (args, rhs) =
@@ -1101,15 +1112,11 @@
       const_syntax c
       |> Option.map (fst o fst)
       |> the_default 0;
-    fun preprocess const_syntax module =
-      module
-      |> debug_msg (fn _ => "eta-expanding...")
-      |> CodegenThingol.eta_expand (eta_expander const_syntax)
   in
     (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
     #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
     >> (fn (seri) => fn (class_syntax, tyco_syntax, const_syntax) => seri 
-         (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax))
+         (class_syntax, tyco_syntax, const_syntax))
   end;
 
 end; (* local *)

--- a/src/Pure/Tools/codegen_thingol.ML	Tue May 09 11:00:32 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue May 09 14:18:40 2006 +0200
@@ -28,7 +28,8 @@
     | IVar of vname
     | `$ of iexpr * iexpr
     | `|-> of (vname * itype) * iexpr
-    | INum of (IntInf.int (*positive!*) * itype) * unit
+    | INum of IntInf.int (*positive!*) * unit
+    | IChar of string (*length one!*) * iexpr
     | IAbs of ((iexpr * itype) * iexpr) * iexpr
         (* (((binding expression (ve), binding type (vty)),
                 body expression (be)), native expression (e0)) *)
@@ -58,6 +59,10 @@
   val add_varnames: iexpr -> string list -> string list;
   val is_pat: 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;
+  
 
   type funn = (iexpr list * iexpr) list * (sortcontext * itype);
   type datatyp = sortcontext * (string * itype list) list;
@@ -98,10 +103,6 @@
     -> string -> transact -> transact;
   val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
 
-  val eta_expand: (string -> int) -> module -> module;
-  val eta_expand_poly: module -> module;
-  val unclash_vars_tvars: module -> module;
-
   val debug: bool ref;
   val debug_msg: ('a -> string) -> 'a -> 'a;
   val soft_exc: bool ref;
@@ -171,7 +172,8 @@
   | IVar of vname
   | `$ of iexpr * iexpr
   | `|-> of (vname * itype) * iexpr
-  | INum of (IntInf.int (*positive!*) * itype) * unit
+  | INum of IntInf.int (*positive!*) * unit
+  | IChar of string (*length one!*) * iexpr
   | IAbs of ((iexpr * itype) * iexpr) * iexpr
   | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
     (*see also signature*)
@@ -225,8 +227,10 @@
   | pretty_iexpr ((v, ty) `|-> e) =
       (Pretty.enclose "(" ")" o Pretty.breaks)
         [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iexpr e]
-  | pretty_iexpr (INum ((n, _), _)) =
+  | pretty_iexpr (INum (n, _)) =
       (Pretty.str o IntInf.toString) n
+  | pretty_iexpr (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]
@@ -272,32 +276,6 @@
   | map_itype f (t1 `-> t2) =
       f t1 `-> f t2;
 
-fun map_iexpr _ (e as IConst _) =
-      e
-  | map_iexpr _ (e as IVar _) =
-      e
-  | map_iexpr f (e1 `$ e2) =
-      f e1 `$ f e2
-  | map_iexpr f ((v, ty) `|-> e) =
-      (v, ty) `|-> f e
-  | map_iexpr _ (e as INum _) =
-      e
-  | map_iexpr f (IAbs (((ve, vty), be), e0)) =
-      IAbs (((f ve, vty), f be), e0)
-  | map_iexpr f (ICase (((de, dty), bses), e0)) =
-      ICase (((f de, dty), map (fn (se, be) => (f se, f be)) bses), e0);
-
-fun map_iexpr_itype f =
-  let
-    fun mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e
-      | mapp (INum ((n, ty), e)) = INum ((n, f ty), e)
-      | mapp (IAbs (((ve, vty), be), e0)) =
-          IAbs (((mapp ve, f vty), mapp be), e0)
-      | mapp (ICase (((de, dty), bses), e0)) =
-          ICase (((mapp de, f dty), map (fn (se, be) => (mapp se, mapp be)) bses), e0)
-      | mapp e = map_iexpr mapp e;
-  in mapp end;
-
 fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) =
   let
     exception NO_MATCH;
@@ -337,6 +315,7 @@
   | is_pat (e as (e1 `$ e2)) =
       is_pat e1 andalso is_pat e2
   | is_pat (e as INum _) = true
+  | is_pat (e as IChar _) = true
   | is_pat e = false;
 
 fun map_pure f (e as IConst _) =
@@ -349,17 +328,15 @@
       f e
   | map_pure _ (INum _) =
       error ("sorry, no pure representation of numerals so far")
+  | map_pure f (IChar (_, e0)) =
+      f e0
   | map_pure f (IAbs (_, e0)) =
       f e0
   | map_pure f (ICase (_, e0)) =
       f e0;
 
-fun has_tyvars (_ `%% tys) =
-      exists has_tyvars tys
-  | has_tyvars (ITyVar _) =
-      true
-  | has_tyvars (ty1 `-> ty2) =
-      has_tyvars ty1 orelse has_tyvars ty2;
+fun resolve_tycos _ = error "";
+fun resolve_consts _ = error "";
 
 fun add_constnames (IConst (c, _)) =
       insert (op =) c
@@ -371,6 +348,8 @@
       add_constnames e
   | add_constnames (INum _) =
       I
+  | add_constnames (IChar _) =
+      I
   | add_constnames (IAbs (_, e)) =
       add_constnames e
   | add_constnames (ICase (_, e)) =
@@ -386,6 +365,8 @@
       insert (op =) v #> add_varnames e
   | add_varnames (INum _) =
       I
+  | add_varnames (IChar _) =
+      I
   | add_varnames (IAbs (((ve, _), be), _)) =
       add_varnames ve #> add_varnames be
   | add_varnames (ICase (((de, _), bses), _)) =
@@ -396,6 +377,14 @@
     val x = Term.variant used seed
   in (x, x :: used) end;
 
+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;
+
 
 
 (** language module system - definitions, modules, transactions **)
@@ -958,69 +947,6 @@
 
 
 
-(** generic transformation **)
-
-fun map_def_fun f (Fun funn) =
-      Fun (f funn)
-  | map_def_fun _ def = def;
-
-fun map_def_fun_expr f (eqs, cty) =
-  (map (fn (ps, rhs) => (map f ps, f rhs)) eqs, cty);
-
-fun eta_expand query =
-  let
-    fun eta e =
-     case unfold_const_app e
-      of SOME (const as (c, (_, ty)), es) =>
-          let
-            val delta = query c - length es;
-            val add_n = if delta < 0 then 0 else delta;
-            val tys =
-              (fst o unfold_fun) ty
-              |> curry Library.drop (length es)
-              |> curry Library.take add_n
-            val vs = (Term.invent_names (fold add_varnames es []) "x" add_n)
-          in
-            vs ~~ tys `|--> IConst const `$$ map eta es `$$ map IVar vs
-          end
-       | NONE => map_iexpr eta e;
-  in (map_defs o map_def_fun o map_def_fun_expr) eta end;
-
-val eta_expand_poly =
-  let
-    fun eta (funn as ([([], e)], cty as (sctxt, (ty as (ty1 `-> ty2))))) =
-          if (not o null) sctxt
-            orelse (not o has_tyvars) ty
-          then funn
-          else (case unfold_abs e
-           of ([], e) =>
-              let
-                val add_var = IVar (hd (Term.invent_names (add_varnames e []) "x" 1))
-              in (([([add_var], e `$ add_var)], cty)) end
-            | _ =>  funn)
-      | eta funn = funn;
-  in (map_defs o map_def_fun) eta end;
-
-val unclash_vars_tvars = 
-  let
-    fun unclash (eqs, (sortctxt, ty)) =
-      let
-        val used_expr =
-          fold (fn (pats, rhs) => fold add_varnames pats #> add_varnames rhs) eqs [];
-        val used_type = map fst sortctxt;
-        val clash = gen_union (op =) (used_expr, used_type);
-        val rename_map = fold_map (fn c => invent c #-> (fn c' => pair (c, c'))) clash [] |> fst;
-        val rename =
-          perhaps (AList.lookup (op =) rename_map);
-        val rename_typ = instant_itype (ITyVar o rename);
-        val rename_expr = map_iexpr_itype rename_typ;
-        fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs)
-      in
-        (map rename_eq eqs, (map (apfst rename) sortctxt, rename_typ ty))
-      end;
-  in (map_defs o map_def_fun) unclash end;
-
-
 (** generic serialization **)
 
 (* resolving *)