# HG changeset patch
# User lcp
# Date 768232163 -7200
# Node ID 5b6e4340085b6fa5b80360495d11d11626f65734
# Parent  796c5e305b319d942e279c47791966f43ba2fca1
ZF/indrule/mk_pred_typ: corrected pattern to include Abs, allowing it to
handle any number of right-nested Sigmas.

diff -r 796c5e305b31 -r 5b6e4340085b src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Fri May 06 15:35:35 1994 +0200
+++ b/src/ZF/indrule.ML	Fri May 06 15:49:23 1994 +0200
@@ -77,7 +77,7 @@
 (*Make distinct predicates for each inductive set*)
 
 (*Sigmas and Cartesian products may nest ONLY to the right!*)
-fun mk_pred_typ (t $ A $ B) = 
+fun mk_pred_typ (t $ A $ Abs(_,_,B)) = 
         if t = Pr.sigma  then  iT --> mk_pred_typ B
                          else  iT --> oT
   | mk_pred_typ _           =  iT --> oT