src/HOL/Tools/Function/partial_function.ML

         Conv.implies_conv split_paired_all_conv Conv.all_conv)
 
     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)))
 
     val inst_rule' = inst_rule
       |> Tactic.rule_by_tactic ctxt
         (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 4
          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
     inst_rule'
   end;