# HG changeset patch # User nipkow # Date 798026171 -7200 # Node ID 5d6fb2c938e0254e63f3cf5196c51896df31701b # Parent d33e3523a5e6ae4034216c3c97f4963a31fb2e38 Fixed bug. diff -r d33e3523a5e6 -r 5d6fb2c938e0 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Sun Apr 16 11:55:03 1995 +0200 +++ b/src/Provers/splitter.ML Sun Apr 16 11:56:11 1995 +0200 @@ -44,16 +44,21 @@ fun add_lbnos(is,t) = add_loose_bnos(t,0,is); -fun typ_test _ [] = true - | typ_test T ((_,U,_)::_) = (T=U); +(* check if the innermost quantifier that needs to be removed + has a body of type T; otherwise the expansion thm will fail later on +*) +fun type_test(T,lbnos,apsns) = + let val (_,U,_) = nth_elem(min lbnos,apsns) + in T=U end; fun mk_split_pack(thm,T,n,ts,apsns) = - if n <= length ts andalso typ_test T apsns - then let val lev = length apsns + if n > length ts then [] + else let val lev = length apsns val lbnos = foldl add_lbnos ([],take(n,ts)) val flbnos = filter (fn i => i < lev) lbnos - in [(thm, if null flbnos then [] else rev apsns)] end - else []; + in if null flbnos then [(thm,[])] + else if type_test(T,flbnos,apsns) then [(thm, rev apsns)] else [] + end; fun split_posns cmap Ts t = let fun posns Ts pos apsns (Abs(_,T,t)) =