diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -200,7 +200,8 @@
     val (P_var, x_var) =
        Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop
       |> strip_comb |> apsnd hd
-    val P_rangeT = range_type (snd (Term.dest_Var P_var))
+      |> apply2 dest_Var
+    val P_rangeT = range_type (snd P_var)
     val PT = map (snd o dest_Free) args ---> P_rangeT
     val x_inst = cert (foldl1 HOLogic.mk_prod args)
     val P_inst = cert (uncurry_n (length args) (Free (P, PT)))
@@ -211,7 +212,7 @@
          THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3
          THEN CONVERSION (split_params_conv ctxt
            then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3)
-      |> Thm.instantiate ([], [(cert P_var, P_inst), (cert x_var, x_inst)]) 
+      |> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)])
       |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
       |> singleton (Variable.export ctxt' ctxt)
   in