--- 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