# HG changeset patch
# User haftmann
# Date 1249977953 -7200
# Node ID 84a6d701e36fa23fccbc2f8c7fa897fd58ce5db7
# Parent  e73eb2db47274969c84e59ddab68c799f579fd85# Parent  e11cd88e6ade0a23abf2061e150ba01e05d32d22
merged

diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -39,6 +39,17 @@
 
 subsubsection {* @{text term_of} instances *}
 
+instantiation "fun" :: (typerep, typerep) term_of
+begin
+
+definition
+  "term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'')
+     [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])"
+
+instance ..
+
+end
+
 setup {*
 let
   fun add_term_of tyco raw_vs thy =
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -444,7 +444,7 @@
   "default" ("(error \"default\")")
   "default :: 'a \<Rightarrow> 'b::default" ("(fn '_ => error \"default\")")
 
-code_module Norm
+(*code_module Norm
 contains
   test = "type_NF"
 
@@ -509,6 +509,6 @@
 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
 val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
-*}
+*}*)
 
 end
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -167,7 +167,7 @@
     val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
   in
     if forall (can dest) thms andalso exists (contains_suc o dest) thms
-      then perhaps_loop (remove_suc thy) thms
+      then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
        else NONE
   end;
 
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -1,12 +1,11 @@
 (*  Title:      HOL/MicroJava/J/JListExample.thy
-    ID:         $Id$
     Author:     Stefan Berghofer
 *)
 
 header {* \isaheader{Example for generating executable code from Java semantics} *}
 
 theory JListExample
-imports Eval SystemClasses
+imports Eval
 begin
 
 ML {* Syntax.ambiguity_level := 100000 *}
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -1,12 +1,13 @@
 (*  Title:      HOL/MicroJava/J/State.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Program State} *}
 
-theory State imports TypeRel Value begin
+theory State
+imports TypeRel Value
+begin
 
 types 
   fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
@@ -19,7 +20,10 @@
 
   init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
  "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
-  
+
+lemma [code] (*manual eta expansion*):
+  "init_vars xs = map_of (map (\<lambda>(n, T). (n, default_val T)) xs)"
+  by (simp add: init_vars_def)
 
 types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
       locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -1,11 +1,12 @@
 (*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
-    ID:         $Id$
     Author:     Stefan Berghofer
 *)
 
 header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
 
-theory JVMListExample imports "../J/SystemClasses" JVMExec begin
+theory JVMListExample
+imports "../J/SystemClasses" JVMExec
+begin
 
 consts
   list_nam :: cnam
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -67,14 +67,18 @@
   val split_const: typ * typ * typ -> term
   val mk_split: term -> term
   val flatten_tupleT: typ -> typ list
-  val mk_tupleT: int list list -> typ list -> typ
-  val strip_tupleT: int list list -> typ -> typ list
+  val mk_tupleT: typ list -> typ
+  val strip_tupleT: typ -> typ list
+  val mk_tuple: term list -> term
+  val strip_tuple: term -> term list
+  val mk_ptupleT: int list list -> typ list -> typ
+  val strip_ptupleT: int list list -> typ -> typ list
   val flat_tupleT_paths: typ -> int list list
-  val mk_tuple: int list list -> typ -> term list -> term
-  val dest_tuple: int list list -> term -> term list
+  val mk_ptuple: int list list -> typ -> term list -> term
+  val strip_ptuple: int list list -> term -> term list
   val flat_tuple_paths: term -> int list list
-  val mk_splits: int list list -> typ -> typ -> term -> term
-  val strip_splits: term -> term * typ list * int list list
+  val mk_psplits: int list list -> typ -> typ -> term -> term
+  val strip_psplits: term -> term * typ list * int list list
   val natT: typ
   val zero: term
   val is_zero: term -> bool
@@ -118,6 +122,8 @@
   val mk_literal: string -> term
   val dest_literal: term -> string
   val mk_typerep: typ -> term
+  val termT: typ
+  val term_of_const: typ -> term
   val mk_term_of: typ -> term -> term
   val reflect_term: term -> term
   val mk_valtermify_app: string -> (string * typ) list -> typ -> term
@@ -321,15 +327,33 @@
 fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
   | flatten_tupleT T = [T];
 
+
+(* tuples with right-fold structure *)
+
+fun mk_tupleT [] = unitT
+  | mk_tupleT Ts = foldr1 mk_prodT Ts;
+
+fun strip_tupleT (Type ("Product_Type.unit", [])) = []
+  | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
+  | strip_tupleT T = [T];
+
+fun mk_tuple [] = unit
+  | mk_tuple ts = foldr1 mk_prod ts;
+
+fun strip_tuple (Const ("Product_Type.Unity", _)) = []
+  | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
+  | strip_tuple t = [t];
+
+
 (* tuples with specific arities
 
-  an "arity" of a tuple is a list of lists of integers
-  ("factors"), denoting paths to subterms that are pairs
+   an "arity" of a tuple is a list of lists of integers,
+   denoting paths to subterms that are pairs
 *)
 
-fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
+fun ptuple_err s = raise TERM (s ^ ": inconsistent use of nested products", []);
 
-fun mk_tupleT ps =
+fun mk_ptupleT ps =
   let
     fun mk p Ts =
       if p mem ps then
@@ -340,12 +364,12 @@
       else (hd Ts, tl Ts)
   in fst o mk [] end;
 
-fun strip_tupleT ps =
+fun strip_ptupleT ps =
   let
     fun factors p T = if p mem ps then (case T of
         Type ("*", [T1, T2]) =>
           factors (1::p) T1 @ factors (2::p) T2
-      | _ => prod_err "strip_tupleT") else [T]
+      | _ => ptuple_err "strip_ptupleT") else [T]
   in factors [] end;
 
 val flat_tupleT_paths =
@@ -355,7 +379,7 @@
       | factors p _ = []
   in factors [] end;
 
-fun mk_tuple ps =
+fun mk_ptuple ps =
   let
     fun mk p T ts =
       if p mem ps then (case T of
@@ -364,16 +388,16 @@
               val (t, ts') = mk (1::p) T1 ts;
               val (u, ts'') = mk (2::p) T2 ts'
             in (pair_const T1 T2 $ t $ u, ts'') end
-        | _ => prod_err "mk_tuple")
+        | _ => ptuple_err "mk_ptuple")
       else (hd ts, tl ts)
   in fst oo mk [] end;
 
-fun dest_tuple ps =
+fun strip_ptuple ps =
   let
     fun dest p t = if p mem ps then (case t of
         Const ("Pair", _) $ t $ u =>
           dest (1::p) t @ dest (2::p) u
-      | _ => prod_err "dest_tuple") else [t]
+      | _ => ptuple_err "strip_ptuple") else [t]
   in dest [] end;
 
 val flat_tuple_paths =
@@ -383,24 +407,24 @@
       | factors p _ = []
   in factors [] end;
 
-(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
+(*In mk_psplits ps S T u, term u expects separate arguments for the factors of S,
   with result type T.  The call creates a new term expecting one argument
   of type S.*)
-fun mk_splits ps T T3 u =
+fun mk_psplits ps T T3 u =
   let
     fun ap ((p, T) :: pTs) =
           if p mem ps then (case T of
               Type ("*", [T1, T2]) =>
                 split_const (T1, T2, map snd pTs ---> T3) $
                   ap ((1::p, T1) :: (2::p, T2) :: pTs)
-            | _ => prod_err "mk_splits")
+            | _ => ptuple_err "mk_psplits")
           else Abs ("x", T, ap pTs)
       | ap [] =
           let val k = length ps
           in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   in ap [([], T)] end;
 
-val strip_splits =
+val strip_psplits =
   let
     fun strip [] qs Ts t = (t, Ts, qs)
       | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
@@ -591,7 +615,9 @@
 
 val termT = Type ("Code_Eval.term", []);
 
-fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
+fun term_of_const T = Const ("Code_Eval.term_of_class.term_of", T --> termT);
+
+fun mk_term_of T t = term_of_const T $ t;
 
 fun reflect_term (Const (c, T)) =
       Const ("Code_Eval.Const", literalT --> typerepT --> termT)
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -645,7 +645,7 @@
 
 fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
     (Const ("Collect", _), [u]) =>
-      let val (r, Ts, fs) = HOLogic.strip_splits u
+      let val (r, Ts, fs) = HOLogic.strip_psplits u
       in case strip_comb r of
           (Const (s, T), ts) =>
             (case (get_clauses thy s, get_assoc_code thy (s, T)) of
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -34,10 +34,10 @@
 val collect_mem_simproc =
   Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
-         let val (u, Ts, ps) = HOLogic.strip_splits t
+         let val (u, Ts, ps) = HOLogic.strip_psplits t
          in case u of
            (c as Const ("op :", _)) $ q $ S' =>
-             (case try (HOLogic.dest_tuple ps) q of
+             (case try (HOLogic.strip_ptuple ps) q of
                 NONE => NONE
               | SOME ts =>
                   if not (loose_bvar (S', 0)) andalso
@@ -80,7 +80,7 @@
       fun mk_collect p T t =
         let val U = HOLogic.dest_setT T
         in HOLogic.Collect_const U $
-          HOLogic.mk_splits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
+          HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
         end;
       fun decomp (Const (s, _) $ ((m as Const ("op :",
             Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
@@ -224,11 +224,11 @@
   map (fn (x, ps) =>
     let
       val U = HOLogic.dest_setT (fastype_of x);
-      val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x
+      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
     in
       (cterm_of thy x,
        cterm_of thy (HOLogic.Collect_const U $
-         HOLogic.mk_splits ps U HOLogic.boolT x'))
+         HOLogic.mk_psplits ps U HOLogic.boolT x'))
     end) fs;
 
 fun mk_to_pred_eq p fs optfs' T thm =
@@ -241,7 +241,7 @@
       | SOME fs' =>
           let
             val (_, U) = split_last (binder_types T);
-            val Ts = HOLogic.strip_tupleT fs' U;
+            val Ts = HOLogic.strip_ptupleT fs' U;
             (* FIXME: should cterm_instantiate increment indexes? *)
             val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
             val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
@@ -249,7 +249,7 @@
           in
             thm' RS (Drule.cterm_instantiate [(arg_cong_f,
               cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
-                HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
+                HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
                   HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
           end)
   in
@@ -362,12 +362,12 @@
     val insts = map (fn (x, ps) =>
       let
         val Ts = binder_types (fastype_of x);
-        val T = HOLogic.mk_tupleT ps Ts;
+        val T = HOLogic.mk_ptupleT ps Ts;
         val x' = map_type (K (HOLogic.mk_setT T)) x
       in
         (cterm_of thy x,
          cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
-           (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
+           (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
       end) fs
   in
     thm |>
@@ -423,14 +423,14 @@
         SOME fs =>
           let
             val T = HOLogic.dest_setT (fastype_of x);
-            val Ts = HOLogic.strip_tupleT fs T;
+            val Ts = HOLogic.strip_ptupleT fs T;
             val x' = map_type (K (Ts ---> HOLogic.boolT)) x
           in
             (x, (x',
               (HOLogic.Collect_const T $
-                 HOLogic.mk_splits fs T HOLogic.boolT x',
+                 HOLogic.mk_psplits fs T HOLogic.boolT x',
                list_abs (map (pair "x") Ts, HOLogic.mk_mem
-                 (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
+                 (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)),
                   x)))))
           end
        | NONE => (x, (x, (x, x))))) params;
@@ -449,13 +449,13 @@
            Pretty.str ("of " ^ s ^ " do not agree with types"),
            Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
            Pretty.str "of declared parameters"]));
-        val Ts = HOLogic.strip_tupleT fs U;
+        val Ts = HOLogic.strip_ptupleT fs U;
         val c' = Free (s ^ "p",
           map fastype_of params1 @ Ts ---> HOLogic.boolT)
       in
         ((c', (fs, U, Ts)),
          (list_comb (c, params2),
-          HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
+          HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT
             (list_comb (c', params1))))
       end) |> split_list |>> split_list;
     val eqns' = eqns @
@@ -485,7 +485,7 @@
     val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
       (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
          fold_rev lambda params (HOLogic.Collect_const U $
-           HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
+           HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
          (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
 
     (* prove theorems for converting predicate to set notation *)
@@ -496,7 +496,7 @@
             (HOLogic.mk_Trueprop (HOLogic.mk_eq
               (list_comb (p, params3),
                list_abs (map (pair "x") Ts, HOLogic.mk_mem
-                 (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
+                 (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
                   list_comb (c, params))))))
             (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
               [def, mem_Collect_eq, split_conv]) 1))
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -40,9 +40,10 @@
   let
     val fun_upd = Const (@{const_name fun_upd},
       (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
-    val (seed', seed'') = random_split seed;
+    val ((y, t2), seed') = random seed;
+    val (seed'', seed''') = random_split seed';
 
-    val state = ref (seed', [], fn () => Const (@{const_name undefined}, T1 --> T2));
+    val state = ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
     fun random_fun' x =
       let
         val (seed, fun_map, f_t) = ! state;
@@ -57,7 +58,7 @@
             in y end
       end;
     fun term_fun' () = #3 (! state) ();
-  in ((random_fun', term_fun'), seed'') end;
+  in ((random_fun', term_fun'), seed''') end;
 
 
 (** type copies **)
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -31,25 +31,18 @@
     |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
   end;
 
-fun expand_eta thy [] = []
-  | expand_eta thy (thms as thm :: _) =
-      let
-        val (_, ty) = Code.const_typ_eqn thy thm;
-      in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
-        then thms
-        else map (Code.expand_eta thy 1) thms
-      end;
-
 fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
   let
     val c' = AxClass.unoverload_const thy (c, T);
     val opt_name = Symtab.lookup (ModuleData.get thy) c';
-    val thms = Code.these_eqns thy c'
-      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
-      |> expand_eta thy
-      |> Code.norm_varnames thy
-      |> map (rpair opt_name)
-  in if null thms then NONE else SOME thms end;
+    val raw_thms = Code.these_eqns thy c'
+      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE);
+  in if null raw_thms then NONE else
+    raw_thms
+    |> Code_Thingol.clean_thms thy (snd (Code.const_typ_eqn thy (hd raw_thms)))
+    |> map (rpair opt_name)
+    |> SOME
+  end;
 
 val dest_eqn = Logic.dest_equals;
 val const_of = dest_Const o head_of o fst o dest_eqn;
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/Tools/split_rule.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -81,7 +81,7 @@
               let
                 val Ts = HOLogic.flatten_tupleT T;
                 val ys = Name.variant_list xs (replicate (length Ts) a);
-              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple (HOLogic.flat_tupleT_paths T) T
+              in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
               end
           | mk_tuple _ x = x;
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -1,61 +1,8 @@
 theory Predicate_Compile
-imports Main Lattice_Syntax Code_Eval RPred
+imports Complex_Main RPred
 uses "predicate_compile.ML"
 begin
 
-text {* Package setup *}
-
 setup {* Predicate_Compile.setup *}
 
-text {* Experimental code *}
-
-ML {*
-structure Predicate_Compile =
-struct
-
-open Predicate_Compile;
-
-fun eval thy t_compr =
-  let
-    val t = Predicate_Compile.analyze_compr thy t_compr;
-    val Type (@{type_name Predicate.pred}, [T]) = fastype_of t;
-    fun mk_predT T = Type (@{type_name Predicate.pred}, [T]);
-    val T1 = T --> @{typ term};
-    val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
-    val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
-      $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
-  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
-
-fun values ctxt k t_compr =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val (T, t') = eval thy t_compr;
-  in t' |> Predicate.yieldn k |> fst |> HOLogic.mk_list T end;
-
-fun values_cmd modes k raw_t state =
-  let
-    val ctxt = Toplevel.context_of state;
-    val t = Syntax.read_term ctxt raw_t;
-    val t' = values ctxt k t;
-    val ty' = Term.type_of t';
-    val ctxt' = Variable.auto_fixes t' ctxt;
-    val p = PrintMode.with_modes modes (fn () =>
-      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
-  in Pretty.writeln p end;
-
-end;
-
-local structure P = OuterParse in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
-  (opt_modes -- Scan.optional P.nat ~1 -- P.term
-    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
-        (Predicate_Compile.values_cmd modes k t)));
-
-end;
-*}
-
 end
\ No newline at end of file
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Aug 11 10:05:53 2009 +0200
@@ -18,15 +18,10 @@
 values 10 "{n. odd n}"
 
 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
-    append_Nil: "append [] xs xs"
-  | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
+    "append [] xs xs"
+  | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
-inductive rev
-where
-"rev [] []"
-| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
-
-code_pred rev .
+code_pred append .
 
 thm append.equation
 
@@ -34,6 +29,15 @@
 values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
 values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}"
 
+inductive rev where
+    "rev [] []"
+  | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
+
+code_pred rev .
+
+thm rev.equation
+
+values "{xs. rev [0, 1, 2, 3::nat] xs}"
 
 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   for f where
@@ -51,17 +55,15 @@
 
 code_pred is_even .
 
-(* TODO: requires to handle abstractions in parameter positions correctly *)
 values 10 "{(ys, zs). partition is_even
   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
-
 values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
 values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
 
 lemma [code_pred_intros]:
-"r a b ==> tranclp r a b"
-"r a b ==> tranclp r b c ==> tranclp r a c"
-by auto
+  "r a b \<Longrightarrow> tranclp r a b"
+  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
+  by auto
 
 code_pred tranclp
 proof -
@@ -76,6 +78,7 @@
 
 thm tranclp.rpred_equation
 *)
+
 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
@@ -83,7 +86,13 @@
 code_pred succ .
 
 thm succ.equation
+
+values 10 "{(m, n). succ n m}"
+values "{m. succ 0 m}"
+values "{m. succ m 0}"
+
 (* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *)
+
 (*
 values 20 "{n. tranclp succ 10 n}"
 values "{n. tranclp succ n 10}"
diff -r e73eb2db4727 -r 84a6d701e36f src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -54,6 +54,7 @@
     mk_sup : term * term -> term,
     mk_if : term -> term,
     mk_not : term -> term,
+    mk_map : typ -> typ -> term -> term -> term,
     lift_pred : term -> term
   };  
   datatype tmode = Mode of mode * int list * tmode option list;
@@ -608,6 +609,7 @@
   mk_not : term -> term,
 (*  funT_of : mode -> typ -> typ, *)
 (*  mk_fun_of : theory -> (string * typ) -> mode -> term, *) 
+  mk_map : typ -> typ -> term -> term -> term,
   lift_pred : term -> term
 };
 
@@ -621,6 +623,7 @@
 fun mk_not (CompilationFuns funs) = #mk_not funs
 (*fun funT_of (CompilationFuns funs) = #funT_of funs*)
 (*fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs*)
+fun mk_map (CompilationFuns funs) = #mk_map funs
 fun lift_pred (CompilationFuns funs) = #lift_pred funs
 
 fun funT_of compfuns (iss, is) T =
@@ -691,12 +694,15 @@
   in
     Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
   end;
-  
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
+  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
+
 val lift_pred = I
 
 val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
   mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
-  lift_pred = lift_pred} 
+  mk_map = mk_map, lift_pred = lift_pred};
 
 end;
 
@@ -748,7 +754,9 @@
   HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
 
 fun mk_not t = error "Negation is not defined for RPred"
-   
+
+fun mk_map t = error "FIXME" (*FIXME*)
+
 fun lift_pred t =
   let
     val T = PredicateCompFuns.dest_predT (fastype_of t)
@@ -759,7 +767,7 @@
 
 val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot,
     mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
-    lift_pred = lift_pred} 
+    mk_map = mk_map, lift_pred = lift_pred};
 
 end;
 (* for external use with interactive mode *)
@@ -2094,18 +2102,17 @@
 
 val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
 
+(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
 fun analyze_compr thy t_compr =
   let
     val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
       | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
-    val (body, Ts, fp) = HOLogic.strip_splits split;
-      (*FIXME former order of tuple positions must be restored*)
-    val (pred as Const (name, T), all_args) = strip_comb body
-    val (params, args) = chop (nparams_of thy name) all_args
+    val (body, Ts, fp) = HOLogic.strip_psplits split;
+    val (pred as Const (name, T), all_args) = strip_comb body;
+    val (params, args) = chop (nparams_of thy name) all_args;
     val user_mode = map_filter I (map_index
       (fn (i, t) => case t of Bound j => if j < length Ts then NONE
-        else SOME (i+1) | _ => SOME (i+1)) args) (*FIXME dangling bounds should not occur*)
-    val (inargs, _) = split_smode user_mode args;
+        else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*)
     val modes = filter (fn Mode (_, is, _) => is = user_mode)
       (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
     val m = case modes
@@ -2114,10 +2121,62 @@
       | [m] => m
       | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
                 ^ Syntax.string_of_term_global thy t_compr); m);
-    val t_eval = list_comb (compile_expr NONE thy 
-      (m, list_comb (pred, params)),
-      inargs)
+    val (inargs, outargs) = split_smode user_mode args;
+    val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs);
+    val t_eval = if null outargs then t_pred else let
+        val outargs_bounds = map (fn Bound i => i) outargs;
+        val outargsTs = map (nth Ts) outargs_bounds;
+        val T_pred = HOLogic.mk_tupleT outargsTs;
+        val T_compr = HOLogic.mk_ptupleT fp Ts;
+        val arrange_bounds = map_index I outargs_bounds
+          |> sort (prod_ord (K EQUAL) int_ord)
+          |> map fst;
+        val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split
+          (Term.list_abs (map (pair "") outargsTs,
+            HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)))
+      in mk_map PredicateCompFuns.compfuns T_pred T_compr arrange t_pred end
   in t_eval end;
 
+fun eval thy t_compr =
+  let
+    val t = analyze_compr thy t_compr;
+    val T = dest_predT PredicateCompFuns.compfuns (fastype_of t);
+    val t' = mk_map PredicateCompFuns.compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
+  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
+
+fun values ctxt k t_compr =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val (T, t) = eval thy t_compr;
+    val setT = HOLogic.mk_setT T;
+    val (ts, _) = Predicate.yieldn k t;
+    val elemsT = HOLogic.mk_set T ts;
+  in if k = ~1 orelse length ts < k then elemsT
+    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
+  end;
+
+fun values_cmd modes k raw_t state =
+  let
+    val ctxt = Toplevel.context_of state;
+    val t = Syntax.read_term ctxt raw_t;
+    val t' = values ctxt k t;
+    val ty' = Term.type_of t';
+    val ctxt' = Variable.auto_fixes t' ctxt;
+    val p = PrintMode.with_modes modes (fn () =>
+      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
+  in Pretty.writeln p end;
+
+local structure P = OuterParse in
+
+val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
+  (opt_modes -- Scan.optional P.nat ~1 -- P.term
+    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
+        (values_cmd modes k t)));
+
 end;
 
+end;
+
diff -r e73eb2db4727 -r 84a6d701e36f src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/Pure/Isar/code.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -33,9 +33,6 @@
     -> (thm * bool) list -> (thm * bool) list
   val const_typ_eqn: theory -> thm -> string * typ
   val typscheme_eqn: theory -> thm -> (string * sort) list * typ
-  val expand_eta: theory -> int -> thm -> thm
-  val norm_args: theory -> thm list -> thm list 
-  val norm_varnames: theory -> thm list -> thm list
 
   (*executable code*)
   val add_datatype: (string * typ) list -> theory -> theory
@@ -126,115 +123,6 @@
   in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end;
 
 
-(* code equation transformations *)
-
-fun expand_eta thy k thm =
-  let
-    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
-    val (head, args) = strip_comb lhs;
-    val l = if k = ~1
-      then (length o fst o strip_abs) rhs
-      else Int.max (0, k - length args);
-    val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
-    fun get_name _ 0 = pair []
-      | get_name (Abs (v, ty, t)) k =
-          Name.variants [v]
-          ##>> get_name t (k - 1)
-          #>> (fn ([v'], vs') => (v', ty) :: vs')
-      | get_name t k = 
-          let
-            val (tys, _) = (strip_type o fastype_of) t
-          in case tys
-           of [] => raise TERM ("expand_eta", [t])
-            | ty :: _ =>
-                Name.variants [""]
-                #-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
-                #>> (fn vs' => (v, ty) :: vs'))
-          end;
-    val (vs, _) = get_name rhs l used;
-    fun expand (v, ty) thm = Drule.fun_cong_rule thm
-      (Thm.cterm_of thy (Var ((v, 0), ty)));
-  in
-    thm
-    |> fold expand vs
-    |> Conv.fconv_rule Drule.beta_eta_conversion
-  end;
-
-fun norm_args thy thms =
-  let
-    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
-    val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
-  in
-    thms
-    |> map (expand_eta thy k)
-    |> map (Conv.fconv_rule Drule.beta_eta_conversion)
-  end;
-
-fun canonical_tvars thy thm =
-  let
-    val ctyp = Thm.ctyp_of thy;
-    val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'";
-    fun tvars_subst_for thm = (fold_types o fold_atyps)
-      (fn TVar (v_i as (v, _), sort) => let
-            val v' = purify_tvar v
-          in if v = v' then I
-          else insert (op =) (v_i, (v', sort)) end
-        | _ => I) (prop_of thm) [];
-    fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
-      let
-        val ty = TVar (v_i, sort)
-      in
-        (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
-      end;
-    val maxidx = Thm.maxidx_of thm + 1;
-    val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
-  in Thm.instantiate (inst, []) thm end;
-
-fun canonical_vars thy thm =
-  let
-    val cterm = Thm.cterm_of thy;
-    val purify_var = Name.desymbolize false;
-    fun vars_subst_for thm = fold_aterms
-      (fn Var (v_i as (v, _), ty) => let
-            val v' = purify_var v
-          in if v = v' then I
-          else insert (op =) (v_i, (v', ty)) end
-        | _ => I) (prop_of thm) [];
-    fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
-      let
-        val t = Var (v_i, ty)
-      in
-        (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
-      end;
-    val maxidx = Thm.maxidx_of thm + 1;
-    val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
-  in Thm.instantiate ([], inst) thm end;
-
-fun canonical_absvars thm =
-  let
-    val t = Thm.plain_prop_of thm;
-    val purify_var = Name.desymbolize false;
-    val t' = Term.map_abs_vars purify_var t;
-  in Thm.rename_boundvars t t' thm end;
-
-fun norm_varnames thy thms =
-  let
-    fun burrow_thms f [] = []
-      | burrow_thms f thms =
-          thms
-          |> Conjunction.intr_balanced
-          |> f
-          |> Conjunction.elim_balanced (length thms)
-  in
-    thms
-    |> map (canonical_vars thy)
-    |> map canonical_absvars
-    |> map Drule.zero_var_indexes
-    |> burrow_thms (canonical_tvars thy)
-    |> Drule.zero_var_indexes_list
-  end;
-
-
 (** data store **)
 
 (* code equations *)
@@ -662,32 +550,21 @@
         ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
   in map (cert o assert_eqn thy) eqns end;
 
-fun common_typ_eqns thy [] = []
-  | common_typ_eqns thy [thm] = [thm]
-  | common_typ_eqns thy (thms as thm :: _) = (*FIXME is too general*)
-      let
-        fun incr_thm thm max =
-          let
-            val thm' = incr_indexes max thm;
-            val max' = Thm.maxidx_of thm' + 1;
-          in (thm', max') end;
-        val (thms', maxidx) = fold_map incr_thm thms 0;
-        val ty1 :: tys = map (snd o const_typ_eqn thy) thms';
-        fun unify ty env = Sign.typ_unify thy (ty1, ty) env
-          handle Type.TUNIFY =>
-            error ("Type unificaton failed, while unifying code equations\n"
-            ^ (cat_lines o map (Display.string_of_thm_global thy)) thms
-            ^ "\nwith types\n"
-            ^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
-        val (env, _) = fold unify tys (Vartab.empty, maxidx)
-        val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
-          cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
-      in map (Thm.instantiate (instT, [])) thms' end;
+fun same_typscheme thy thms =
+  let
+    fun tvars_of t = rev (Term.add_tvars t []);
+    val vss = map (tvars_of o Thm.prop_of) thms;
+    fun inter_sorts vs =
+      fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
+    val sorts = map_transpose inter_sorts vss;
+    val vts = Name.names Name.context Name.aT sorts
+      |> map (fn (v, sort) => TVar ((v, 0), sort));
+  in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
 
 fun these_eqns thy c =
   get_eqns thy c
   |> (map o apfst) (Thm.transfer thy)
-  |> burrow_fst (common_typ_eqns thy);
+  |> burrow_fst (same_typscheme thy);
 
 fun all_eqns thy =
   Symtab.dest ((the_eqns o the_exec) thy)
diff -r e73eb2db4727 -r 84a6d701e36f src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/Pure/Isar/overloading.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -132,36 +132,42 @@
   |> get_first (fn ((c, _), (v, checked)) =>
       if Binding.name_of b = v then SOME (c, checked) else NONE);
 
-fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b));
+
+(* target *)
 
+fun synchronize_syntax ctxt =
+  let
+    val overloading = OverloadingData.get ctxt;
+    fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
+     of SOME (v, _) => SOME (ty, Free (v, ty))
+      | NONE => NONE;
+    val unchecks =
+      map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
+  in 
+    ctxt
+    |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
+  end
 
-(* overloaded declarations and definitions *)
+fun init raw_overloading thy =
+  let
+    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
+    val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
+  in
+    thy
+    |> ProofContext.init
+    |> OverloadingData.put overloading
+    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
+    |> add_improvable_syntax
+    |> synchronize_syntax
+  end;
 
 fun declare c_ty = pair (Const c_ty);
 
 fun define checked b (c, t) = Thm.add_def (not checked) true
   (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
 
-
-(* target *)
-
-fun init raw_overloading thy =
-  let
-    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
-    val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
-    fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
-     of SOME (v, _) => SOME (ty, Free (v, ty))
-      | NONE => NONE;
-    val unchecks =
-      map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
-  in
-    thy
-    |> ProofContext.init
-    |> OverloadingData.put overloading
-    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
-    |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
-    |> add_improvable_syntax
-  end;
+fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
+  #> LocalTheory.target synchronize_syntax
 
 fun conclude lthy =
   let
diff -r e73eb2db4727 -r 84a6d701e36f src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/Pure/library.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -109,6 +109,7 @@
   val split_list: ('a * 'b) list -> 'a list * 'b list
   val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+  val map_transpose: ('a list -> 'b) -> 'a list list -> 'b list
   val separate: 'a -> 'a list -> 'a list
   val surround: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
@@ -929,6 +930,17 @@
   in dups end;
 
 
+(* matrices *)
+
+fun map_transpose f xss =
+  let
+    val n = case distinct (op =) (map length xss)
+     of [] => 0
+      | [n] => n
+      | _ => raise UnequalLengths;
+  in map (fn m => f (map (fn xs => nth xs m) xss)) (0 upto n - 1) end;
+
+
 
 (** lists as multisets **)
 
diff -r e73eb2db4727 -r 84a6d701e36f src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -109,7 +109,10 @@
   | apply_functrans thy c [] eqns = eqns
   | apply_functrans thy c functrans eqns = eqns
       |> perhaps (perhaps_loop (perhaps_apply functrans))
-      |> Code.assert_eqns_const thy c;
+      |> Code.assert_eqns_const thy c
+      (*FIXME in future, the check here should be more accurate wrt. type schemes
+      -- perhaps by means of upcoming code certificates with a corresponding
+         preprocessor protocol*);
 
 fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
 
@@ -140,8 +143,6 @@
     |> (map o apfst) (rewrite_eqn pre)
     |> (map o apfst) (AxClass.unoverload thy)
     |> map (Code.assert_eqn thy)
-    |> burrow_fst (Code.norm_args thy)
-    |> burrow_fst (Code.norm_varnames thy)
   end;
 
 fun preprocess_conv thy ct =
diff -r e73eb2db4727 -r 84a6d701e36f src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Aug 10 18:12:55 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Aug 11 10:05:53 2009 +0200
@@ -79,6 +79,7 @@
   val is_cons: program -> string -> bool
   val contr_classparam_typs: program -> string -> itype option list
 
+  val clean_thms: theory -> typ -> thm list -> thm list
   val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
@@ -376,6 +377,67 @@
 end; (* local *)
 
 
+(** technical transformations of code equations **)
+
+fun expand_eta thy k thm =
+  let
+    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
+    val (head, args) = strip_comb lhs;
+    val l = if k = ~1
+      then (length o fst o strip_abs) rhs
+      else Int.max (0, k - length args);
+    val (raw_vars, _) = Term.strip_abs_eta l rhs;
+    val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs [])))
+      raw_vars;
+    fun expand (v, ty) thm = Drule.fun_cong_rule thm
+      (Thm.cterm_of thy (Var ((v, 0), ty)));
+  in
+    thm
+    |> fold expand vars
+    |> Conv.fconv_rule Drule.beta_eta_conversion
+  end;
+
+fun same_arity thy thms =
+  let
+    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
+    val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
+  in map (expand_eta thy k) thms end;
+
+fun avoid_value thy ty [thm] =
+      if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
+      then [thm]
+      else [expand_eta thy 1 thm]
+  | avoid_value thy _ thms = thms;
+
+fun mk_desymbolization pre post mk vs =
+  let
+    val names = map (pre o fst o fst) vs
+      |> map (Name.desymbolize false)
+      |> Name.variant_list []
+      |> map post;
+  in map_filter (fn (((v, i), x), v') =>
+    if v = v' andalso i = 0 then NONE
+    else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
+  end;
+
+fun desymbolize_tvars thy thms =
+  let
+    val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
+    val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
+  in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
+
+fun desymbolize_vars thy thm =
+  let
+    val vs = Term.add_vars (Thm.prop_of thm) [];
+    val var_subst = mk_desymbolization I I Var vs;
+  in Thm.certify_instantiate ([], var_subst) thm end;
+
+fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy);
+
+fun clean_thms thy ty =
+  same_arity thy #> avoid_value thy ty #> desymbolize_all_vars thy;
+
+
 (** statements, abstract programs **)
 
 type typscheme = (vname * sort) list * itype;
@@ -498,17 +560,11 @@
     fun stmt_classparam class =
       ensure_class thy algbr funcgr class
       #>> (fn class => Classparam (c, class));
-    fun stmt_fun ((vs, ty), raw_thms) =
-      let
-        val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
-          then raw_thms
-          else (map o apfst) (Code.expand_eta thy 1) raw_thms;
-      in
-        fold_map (translate_tyvar_sort thy algbr funcgr) vs
-        ##>> translate_typ thy algbr funcgr ty
-        ##>> fold_map (translate_eq thy algbr funcgr) thms
-        #>> (fn info => Fun (c, info))
-      end;
+    fun stmt_fun ((vs, ty), eqns) =
+      fold_map (translate_tyvar_sort thy algbr funcgr) vs
+      ##>> translate_typ thy algbr funcgr ty
+      ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy ty) eqns)
+      #>> (fn info => Fun (c, info));
     val stmt_const = case Code.get_datatype_of_constr thy c
      of SOME tyco => stmt_datatypecons tyco
       | NONE => (case AxClass.class_of_param thy c
@@ -597,7 +653,7 @@
             translate_term thy algbr funcgr thm t'
             ##>> fold_map (translate_term thy algbr funcgr thm) ts
             #>> (fn (t, ts) => t `$$ ts)
-and translate_eq thy algbr funcgr (thm, proper) =
+and translate_eqn thy algbr funcgr (thm, proper) =
   let
     val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
       o Logic.unvarify o prop_of) thm;