diff -r 4736ff5a41d8 -r 588b81d19823 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Wed Jan 28 11:17:21 2015 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Jan 28 12:26:56 2015 +0100
@@ -248,15 +248,18 @@
 
 fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs, ...}) =
   let
-    val arg_vars = 
-      cargTs
-      |> map_index (fn (i, T) => Free ("x" ^ string_of_int i, T)) (* FIXME: proper context *)
+    val name_ctxt = Variable.names_of ctxt
+    fun mk_var x T ctxt = case Name.variant x ctxt of (x, ctxt) => (Free (x, T), ctxt)
+    val (arg_vars, name_ctxt) = fold_index 
+          (fn (i, T) => fn (acc, ctxt) =>
+            case mk_var ("x" ^ string_of_int i) T ctxt of (x, ctxt) => (x :: acc, ctxt))
+          cargTs ([], name_ctxt)
 
     val argsT = fastype_of (HOLogic.mk_tuple arg_vars)
-    val args = Free ("x", argsT) (* FIXME: proper context *)
-
+    val (args, name_ctxt) = mk_var "x" argsT name_ctxt
+    
     val cert = cterm_of (Proof_Context.theory_of ctxt)
-
+    val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> cert
     val sumtree_inj = Sum_Tree.mk_inj ST n i args
 
     val sum_elims =
@@ -267,11 +270,11 @@
       THEN REPEAT (Tactic.eresolve_tac sum_elims i)
   in
     cases_rule
-    |> Thm.forall_elim @{cterm "P::bool"}
+    |> Thm.forall_elim P
     |> Thm.forall_elim (cert sumtree_inj)
     |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal)
     |> Thm.forall_intr (cert args)
-    |> Thm.forall_intr @{cterm "P::bool"}
+    |> Thm.forall_intr P
   end