diff -r e7c0ca878120 -r 42079156c5aa src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sun May 31 00:11:12 2015 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun May 31 00:16:26 2015 +0200
@@ -250,7 +250,7 @@
     val [P, x] =
       Variable.variant_frees ctxt [] [("P", @{typ bool}), ("x", HOLogic.mk_tupleT Ts)]
       |> map (Thm.cterm_of ctxt o Free);
-    val sumtree_inj = Drule.cterm_fun (Sum_Tree.mk_inj ST n i) x;
+    val sumtree_inj = Thm.cterm_of ctxt (Sum_Tree.mk_inj ST n i (Thm.term_of x));
 
     fun prep_subgoal_tac i =
       REPEAT (eresolve_tac ctxt