src/Provers/splitter.ML
changeset 1064 5d6fb2c938e0
parent 1030 1d8fa2fc4b9c
child 1686 c67d543bc395
     1.1 --- a/src/Provers/splitter.ML	Sun Apr 16 11:55:03 1995 +0200
     1.2 +++ b/src/Provers/splitter.ML	Sun Apr 16 11:56:11 1995 +0200
     1.3 @@ -44,16 +44,21 @@
     1.4  
     1.5  fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
     1.6  
     1.7 -fun typ_test _ [] = true
     1.8 -  | typ_test T ((_,U,_)::_) = (T=U);
     1.9 +(* check if the innermost quantifier that needs to be removed
    1.10 +   has a body of type T; otherwise the expansion thm will fail later on
    1.11 +*)
    1.12 +fun type_test(T,lbnos,apsns) =
    1.13 +  let val (_,U,_) = nth_elem(min lbnos,apsns)
    1.14 +  in T=U end;
    1.15  
    1.16  fun mk_split_pack(thm,T,n,ts,apsns) =
    1.17 -  if n <= length ts andalso typ_test T apsns
    1.18 -  then let val lev = length apsns
    1.19 +  if n > length ts then []
    1.20 +  else let val lev = length apsns
    1.21             val lbnos = foldl add_lbnos ([],take(n,ts))
    1.22             val flbnos = filter (fn i => i < lev) lbnos
    1.23 -       in [(thm, if null flbnos then [] else rev apsns)] end
    1.24 -  else [];
    1.25 +       in if null flbnos then [(thm,[])]
    1.26 +          else if type_test(T,flbnos,apsns) then [(thm, rev apsns)] else []
    1.27 +       end;
    1.28  
    1.29  fun split_posns cmap Ts t =
    1.30    let fun posns Ts pos apsns (Abs(_,T,t)) =