normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
tuned naming;
dropped dead parameters;

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu May 08 21:17:23 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri May 09 08:13:26 2014 +0200
@@ -305,9 +305,9 @@
 
 fun dynamic_value_strict opts cookie ctxt postproc t =
   let
-    fun evaluator program ((_, vs_ty), t) deps =
+    fun evaluator program _ vs_ty_t deps =
       Exn.interruptible_capture (value opts ctxt cookie)
-        (Code_Target.evaluator ctxt target program deps true (vs_ty, t));
+        (Code_Target.evaluator ctxt target program deps true vs_ty_t);
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end;
 
 (** counterexample generator **)

--- a/src/Tools/Code/code_preproc.ML	Thu May 08 21:17:23 2014 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri May 09 08:13:26 2014 +0200
@@ -24,14 +24,14 @@
   val pretty: Proof.context -> code_graph -> Pretty.T
   val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
   val dynamic_conv: Proof.context
-    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
+    -> (code_algebra -> code_graph -> term -> conv) -> conv
   val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a)
-    -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
+    -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'a
   val static_conv: Proof.context -> string list
-    -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> conv)
+    -> (code_algebra -> code_graph -> Proof.context -> term -> conv)
     -> Proof.context -> conv
   val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list
-    -> (code_algebra -> code_graph -> Proof.context -> (string * sort) list -> term -> 'a)
+    -> (code_algebra -> code_graph -> Proof.context -> term -> 'a)
     -> Proof.context -> term -> 'a
 
   val setup: theory -> theory
@@ -462,17 +462,15 @@
   (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy)
     (extend_arities_eqngr (Proof_Context.init_global thy) consts ts));
 
-fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
-
 fun dynamic_conv ctxt conv = no_variables_conv ctxt (fn ct =>
   let
     val thm1 = preprocess_conv ctxt ctxt ct;
     val ct' = Thm.rhs_of thm1;
-    val (vs', t') = dest_cterm ct';
+    val t' = Thm.term_of ct';
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
     val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
-    val thm2 = conv algebra' eqngr' vs' t' ct';
+    val thm2 = conv algebra' eqngr' t' ct';
     val thm3 = postprocess_conv ctxt ctxt (Thm.rhs_of thm2);
   in
     Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
@@ -483,13 +481,12 @@
 fun dynamic_value ctxt postproc evaluator t =
   let
     val (resubst, t') = preprocess_term ctxt ctxt t;
-    val vs' = Term.add_tfrees t' [];
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
     val (algebra', eqngr') = obtain false (Proof_Context.theory_of ctxt) consts [t'];
   in
     t'
-    |> evaluator algebra' eqngr' vs'
+    |> evaluator algebra' eqngr'
     |> postproc (postprocess_term ctxt ctxt o resubst)
   end;
 
@@ -500,7 +497,7 @@
     val conv' = conv algebra eqngr;
     val post_conv = postprocess_conv ctxt;
   in fn ctxt' => no_variables_conv ctxt' ((pre_conv ctxt')
-    then_conv (fn ct => uncurry (conv' ctxt') (dest_cterm ct) ct)
+    then_conv (fn ct => conv' ctxt' (Thm.term_of ct) ct)
     then_conv (post_conv ctxt'))
   end;
 
@@ -513,7 +510,7 @@
   in fn ctxt' => 
     preproc ctxt'
     #-> (fn resubst => fn t => t
-      |> evaluator' ctxt' (Term.add_tfrees t [])
+      |> evaluator' ctxt'
       |> postproc (postproc' ctxt' o resubst))
   end;
 

--- a/src/Tools/Code/code_runtime.ML	Thu May 08 21:17:23 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri May 09 08:13:26 2014 +0200
@@ -112,8 +112,8 @@
     val _ = if ! trace
       then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
       else ()
-    fun evaluator program ((_, vs_ty), t) deps =
-      evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) (vs_ty, t) args;
+    fun evaluator program _ vs_ty_t deps =
+      evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args;
   in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end;
 
 fun dynamic_value_strict cookie ctxt some_target postproc t args =
@@ -126,7 +126,7 @@
   let
     val evaluator = obtain_evaluator ctxt some_target program (map Constant consts');
     val evaluation' = evaluation cookie ctxt evaluator;
-  in fn _ => fn ((_, vs_ty), t) => fn _ => evaluation' (vs_ty, t) [] end;
+  in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end;
 
 fun static_value_exn cookie ctxt some_target postproc consts =
   let
@@ -175,14 +175,14 @@
   (Thm.add_oracle (@{binding holds_by_evaluation},
   fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)));
 
-fun check_holds_oracle ctxt evaluator ((_, vs_ty), t) deps ct =
-  raw_check_holds_oracle (ctxt, evaluator, (vs_ty, t), ct);
+fun check_holds_oracle ctxt evaluator vs_ty_t ct =
+  raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct);
 
 in
 
 fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
-  (fn program => fn vs_t => fn deps =>
-    check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t deps)
+  (fn program => fn _ => fn vs_t => fn deps =>
+    check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t)
       o reject_vars ctxt;
 
 fun static_holds_conv ctxt consts =
@@ -190,7 +190,7 @@
     let
       val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts')
     in
-      fn ctxt' => fn vs_t => fn deps => check_holds_oracle ctxt' evaluator' vs_t deps o reject_vars ctxt'
+      fn ctxt' => fn _ => fn vs_t => fn _ => check_holds_oracle ctxt' evaluator' vs_t o reject_vars ctxt'
     end);
 
 (* o reject_vars ctxt'*)

--- a/src/Tools/Code/code_simp.ML	Thu May 08 21:17:23 2014 +0200
+++ b/src/Tools/Code/code_simp.ML	Fri May 09 08:13:26 2014 +0200
@@ -76,7 +76,7 @@
 (* evaluation with dynamic code context *)
 
 fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt
-  (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
+  (fn program => fn _ => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
 
 fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt)
   THEN' conclude_tac ctxt NONE ctxt;
@@ -96,7 +96,7 @@
 fun static_conv ctxt some_ss consts =
   Code_Thingol.static_conv_simple ctxt consts
     (fn program => let val conv' = rewrite_modulo ctxt some_ss program
-     in fn ctxt' => fn _ => fn _ => conv' ctxt' end);
+     in fn ctxt' => fn _ => conv' ctxt' end);
 
 fun static_tac ctxt some_ss consts =
   let

--- a/src/Tools/Code/code_target.ML	Thu May 08 21:17:23 2014 +0200
+++ b/src/Tools/Code/code_target.ML	Fri May 09 08:13:26 2014 +0200
@@ -428,7 +428,7 @@
     else Isabelle_System.with_tmp_dir "Code_Test" ext_check
   end;
 
-fun evaluation mounted_serializer prepared_program syms all_public ((vs, ty), t) =
+fun subevaluator mounted_serializer prepared_program syms all_public ((vs, ty), t) =
   let
     val _ = if Code_Thingol.contains_dict_var t then
       error "Term to be evaluated contains free dictionaries" else ();
@@ -449,7 +449,7 @@
   let
     val (mounted_serializer, (_, prepared_program)) =
       mount_serializer ctxt target NONE generatedN [] program syms;
-  in evaluation mounted_serializer prepared_program syms end;
+  in subevaluator mounted_serializer prepared_program syms end;
 
 end; (* local *)
 

--- a/src/Tools/Code/code_thingol.ML	Thu May 08 21:17:23 2014 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri May 09 08:13:26 2014 +0200
@@ -86,20 +86,20 @@
   val read_const_exprs: Proof.context -> string list -> string list
   val consts_program: theory -> string list -> program
   val dynamic_conv: Proof.context -> (program
-    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
+    -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv)
     -> conv
   val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
-    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
+    -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     -> term -> 'a
   val static_conv: Proof.context -> string list -> (program -> string list
-    -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
+    -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv)
     -> Proof.context -> conv
   val static_conv_simple: Proof.context -> string list
-    -> (program -> Proof.context -> (string * sort) list -> term -> conv)
+    -> (program -> Proof.context -> term -> conv)
     -> Proof.context -> conv
   val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list ->
     (program -> string list
-      -> Proof.context -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
+      -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     -> Proof.context -> term -> 'a
 end;
 
@@ -388,7 +388,7 @@
 
 exception PERMISSIVE of unit;
 
-fun translation_error ctxt program permissive some_thm deps msg sub_msg =
+fun translation_error ctxt permissive some_thm deps msg sub_msg =
   if permissive
   then raise PERMISSIVE ()
   else
@@ -408,14 +408,14 @@
 fun maybe_permissive f prgrm =
   f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm);
 
-fun not_wellsorted ctxt program permissive some_thm deps ty sort e =
+fun not_wellsorted ctxt permissive some_thm deps ty sort e =
   let
     val err_class = Sorts.class_error (Context.pretty ctxt) e;
     val err_typ =
       "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
         Syntax.string_of_sort ctxt sort;
   in
-    translation_error ctxt program permissive some_thm deps
+    translation_error ctxt permissive some_thm deps
       "Wellsortedness error" (err_typ ^ "\n" ^ err_class)
   end;
 
@@ -483,7 +483,7 @@
       {class_relation = K (Sorts.classrel_derivation algebra class_relation),
        type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
-      handle Sorts.CLASS_ERROR e => not_wellsorted ctxt program permissive some_thm deps ty sort e;
+      handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e;
   in (typarg_witnesses, (deps, program)) end;
 
 
@@ -630,7 +630,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
         andalso Code.is_abstr thy c
-        then translation_error ctxt program permissive some_thm deps
+        then translation_error ctxt permissive some_thm deps
           "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
       else ()
   in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end
@@ -795,11 +795,18 @@
 
 (* value evaluation *)
 
-fun ensure_value ctxt algbr eqngr t =
+fun normalize_tvars t = 
   let
     val ty = fastype_of t;
-    val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
+    val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
+    val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
+    val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
+  in ((vs_original, (vs_normalized, normalize ty)), map_types normalize t) end;
+
+fun ensure_value ctxt algbr eqngr t_original =
+  let
+    val ((vs_original, (vs, ty)), t) = normalize_tvars t_original;
     val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t;
     val dummy_constant = Constant @{const_name Pure.dummy_pattern};
     val stmt_value =
@@ -808,29 +815,27 @@
       ##>> translate_term ctxt algbr eqngr false NONE (t', NONE)
       #>> (fn ((vs, ty), t) => Fun
         (((vs, ty), [(([], t), (NONE, true))]), NONE));
-    fun term_value (deps, program1) =
+    fun term_value (_, program1) =
       let
-        val Fun ((vs_ty, [(([], t), _)]), _) =
+        val Fun ((vs_ty as (vs, _), [(([], t), _)]), _) =
           Code_Symbol.Graph.get_node program1 dummy_constant;
         val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
         val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
         val deps_all = Code_Symbol.Graph.all_succs program2 deps';
         val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
-      in ((program3, ((vs_ty, t), deps')), (deps, program2)) end;
+        val vs_mapping = map fst vs ~~ vs_original;
+      in (((the o AList.lookup (op =) vs_mapping), (program3, ((vs_ty, t), deps'))), (deps', program2)) end;
   in
     ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern}
     #> snd
     #> term_value
   end;
 
-fun original_sorts vs =
-  map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v));
-
-fun dynamic_evaluator ctxt evaluator algebra eqngr vs t =
+fun dynamic_evaluator ctxt evaluator algebra eqngr t =
   let
-    val ((program, (((vs', ty'), t'), deps)), _) =
+    val ((resubst_tvar, (program, ((vs_ty', t'), deps))), _) =
       invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
-  in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end;
+  in evaluator program resubst_tvar (vs_ty', t') deps end;
 
 fun dynamic_conv ctxt conv =
   Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt conv);
@@ -838,22 +843,22 @@
 fun dynamic_value ctxt postproc evaluator =
   Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
 
-fun lift_evaluation ctxt evaluation algebra eqngr program vs t =
+fun static_subevaluator ctxt subevaluator algebra eqngr program t =
   let
-    val ((_, (((vs', ty'), t'), deps)), _) =
+    val ((resubst_tvar, (_, ((vs_ty', t'), deps))), _) =
       ensure_value ctxt algebra eqngr t ([], program);
-  in evaluation ctxt ((original_sorts vs vs', (vs', ty')), t') deps end;
+  in subevaluator ctxt resubst_tvar (vs_ty', t') deps end;
 
-fun lift_evaluator ctxt evaluator consts algebra eqngr =
+fun static_evaluator ctxt evaluator consts algebra eqngr =
   let
     fun generate_consts ctxt algebra eqngr =
       fold_map (ensure_const ctxt algebra eqngr false);
     val (consts', program) =
       invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
-    val evaluation = evaluator program consts';
-  in fn ctxt' => lift_evaluation ctxt' evaluation algebra eqngr program end;
+    val subevaluator = evaluator program consts';
+  in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
 
-fun lift_evaluator_simple ctxt evaluator consts algebra eqngr =
+fun static_evaluator_simple ctxt evaluator consts algebra eqngr =
   let
     fun generate_consts ctxt algebra eqngr =
       fold_map (ensure_const ctxt algebra eqngr false);
@@ -862,13 +867,13 @@
   in evaluator program end;
 
 fun static_conv ctxt consts conv =
-  Code_Preproc.static_conv ctxt consts (lift_evaluator ctxt conv consts);
+  Code_Preproc.static_conv ctxt consts (static_evaluator ctxt conv consts);
 
 fun static_conv_simple ctxt consts conv =
-  Code_Preproc.static_conv ctxt consts (lift_evaluator_simple ctxt conv consts);
+  Code_Preproc.static_conv ctxt consts (static_evaluator_simple ctxt conv consts);
 
 fun static_value ctxt postproc consts evaluator =
-  Code_Preproc.static_value ctxt postproc consts (lift_evaluator ctxt evaluator consts);
+  Code_Preproc.static_value ctxt postproc consts (static_evaluator ctxt evaluator consts);
 
 
 (** constant expressions **)

--- a/src/Tools/nbe.ML	Thu May 08 21:17:23 2014 +0200
+++ b/src/Tools/nbe.ML	Fri May 09 08:13:26 2014 +0200
@@ -502,10 +502,11 @@
 
 (* reconstruction *)
 
-fun typ_of_itype vs (tyco `%% itys) =
-      Type (tyco, map (typ_of_itype vs) itys)
-  | typ_of_itype vs (ITyVar v) =
-      TFree ("'" ^ v, (the o AList.lookup (op =) vs) v);
+fun typ_of_itype resubst_tvar =
+  let
+    fun typ_of (tyco `%% itys) = Type (tyco, map typ_of itys)
+      | typ_of (ITyVar v) = TFree (resubst_tvar v);
+  in typ_of end;
 
 fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t =
   let
@@ -542,11 +543,11 @@
 
 (* evaluation with type reconstruction *)
 
-fun eval_term raw_ctxt (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
+fun eval_term raw_ctxt (nbe_program, idx_tab) resubst_tvar ((vs, ty), t) deps =
   let
     val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
     val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
-    val ty' = typ_of_itype vs0 ty;
+    val ty' = typ_of_itype resubst_tvar ty;
     fun type_infer t =
       Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
         (Type.constraint ty' t);
@@ -592,11 +593,11 @@
 
 val (_, raw_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (@{binding normalization_by_evaluation},
-    fn (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
-      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab vsp_ty_t deps))));
+    fn (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct) =>
+      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps))));
 
-fun oracle ctxt nbe_program_idx_tab vsp_ty_t deps ct =
-  raw_oracle (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct);
+fun oracle ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps ct =
+  raw_oracle (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct);
 
 fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
   (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));