misc tuning and simplification;

--- a/src/HOL/Tools/Function/function_elims.ML	Sun Mar 08 21:03:22 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML	Sun Mar 08 21:54:15 2015 +0100
@@ -61,7 +61,7 @@
 fun bool_subst_tac ctxt i =
   REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eq_bool i)
   THEN REPEAT (dresolve_tac ctxt boolD i)
-  THEN REPEAT (eresolve_tac ctxt boolE i)
+  THEN REPEAT (eresolve_tac ctxt boolE i);
 
 fun mk_bool_elims ctxt elim =
   let
@@ -81,16 +81,18 @@
     val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
     val n_fs = length fs;
 
+    fun variant_free used_term v =
+      Free (singleton (Variable.variant_frees ctxt [used_term]) v);
+
     fun mk_partial_elim_rule (idx, f) =
       let
-        fun mk_var x T ctxt = case Name.variant x ctxt of (x, ctxt) => (Free (x, T), ctxt)
-        fun mk_funeq 0 T ctxt (acc_vars, acc_lhs) =
-              let val (y, ctxt) = mk_var "y" T ctxt
-              in  (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T, ctxt) end
-          | mk_funeq n (Type (@{type_name "fun"}, [S, T])) ctxt (acc_vars, acc_lhs) =
-              let val (xn, ctxt) = mk_var "x" S ctxt
-              in  mk_funeq (n - 1) T ctxt (xn :: acc_vars, acc_lhs $ xn) end
-          | mk_funeq _ _ _ _ = raise TERM ("Not a function", [f]);
+        fun mk_funeq 0 T (acc_args, acc_lhs) =
+              let val y = variant_free acc_lhs ("y", T)
+              in (y, rev acc_args, HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))) end
+          | mk_funeq n (Type (@{type_name fun}, [S, T])) (acc_args, acc_lhs) =
+              let val x = variant_free acc_lhs ("x", S)
+              in mk_funeq (n - 1) T (x :: acc_args, acc_lhs $ x) end
+          | mk_funeq _ _ _ = raise TERM ("Not a function", [f]);
 
         val f_simps =
           filter (fn r =>
@@ -108,14 +110,12 @@
           |> snd o fst o dest_funprop
           |> length;
 
-        val name_ctxt = Variable.names_of ctxt
-        val (free_vars, prop, ranT, name_ctxt) = mk_funeq arity (fastype_of f) name_ctxt ([], f);
-        val (rhs_var, arg_vars) = (case free_vars of x :: xs => (x, rev xs));
+        val (rhs_var, arg_vars, prop) = mk_funeq arity (fastype_of f) ([], f);
         val args = HOLogic.mk_tuple arg_vars;
         val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
 
-        val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Thm.cterm_of ctxt
-        val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
+        val P = Thm.cterm_of ctxt (variant_free prop ("P", @{typ bool}));
+        val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx + 1) args;
 
         val cprop = Thm.cterm_of ctxt prop;
 
@@ -138,7 +138,7 @@
           |> Thm.forall_intr (Thm.cterm_of ctxt rhs_var);
 
         val bool_elims =
-          (case ranT of
+          (case fastype_of rhs_var of
             Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
           | _ => []);