# HG changeset patch
# User krauss
# Date 1363909154 -3600
# Node ID 49eb8d73ae10f48a9685839cdf4d9e85be790df8
# Parent  a981a5c8a505f895fdae2b9ae83a42532b730a18
allow induction predicates with arbitrary arity (not just binary)

diff -r a981a5c8a505 -r 49eb8d73ae10 src/HOL/Tools/Function/partial_function.ML
--- 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)))