--- a/src/HOL/Tools/Function/partial_function.ML Thu Mar 21 16:58:14 2013 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Fri Mar 22 00:39:14 2013 +0100
@@ -178,10 +178,10 @@
val inst_rule =
cterm_instantiate' [SOME cuncurry, NONE, SOME ccurry] rule
- val plain_resultT =
- Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop
- |> Term.head_of |> Term.dest_Var |> snd |> range_type |> domain_type
- val PT = map (snd o dest_Free) args ---> plain_resultT --> HOLogic.boolT
+ val P_rangeT =
+ Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop
+ |> Term.head_of |> Term.dest_Var |> snd |> range_type
+ 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)))