# HG changeset patch
# User berghofe
# Date 1202949090 -3600
# Node ID 728f2c325ed6a15f44c8716c9bd0cf3375328a99
# Parent  19df083a2bbf25ff072753b7ddbccef596037b58
Fixed typing problem that caused instantiation of induct_aux_rec to go wrong.

diff -r 19df083a2bbf -r 728f2c325ed6 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Feb 13 15:14:17 2008 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Feb 14 01:31:30 2008 +0100
@@ -1644,7 +1644,7 @@
             Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
               fresh_fs @
           map (fn (((P, T), (x, U)), Q) =>
-           (Var ((P, 0), HOLogic.unitT --> Logic.varifyT T --> HOLogic.boolT),
+           (Var ((P, 0), Logic.varifyT (fsT' --> T --> HOLogic.boolT)),
             Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
               (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
           map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T)))