src/FOLP/simp.ML
changeset 33955 fff6f11b1f09
parent 33339 d41f77196338
child 35021 c839a4c670c6
     1.1 --- a/src/FOLP/simp.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/FOLP/simp.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -419,11 +419,11 @@
     1.4      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
     1.5      else case Seq.pull(cong_tac i thm) of
     1.6              SOME(thm',_) =>
     1.7 -                    let val ps = prems_of thm and ps' = prems_of thm';
     1.8 +                    let val ps = prems_of thm
     1.9 +                        and ps' = prems_of thm';
    1.10                          val n = length(ps')-length(ps);
    1.11                          val a = length(Logic.strip_assums_hyp(List.nth(ps,i-1)))
    1.12 -                        val l = map (fn p => length(Logic.strip_assums_hyp(p)))
    1.13 -                                    (Library.take(n,Library.drop(i-1,ps')));
    1.14 +                        val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps'));
    1.15                      in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
    1.16            | NONE => (REW::ss,thm,anet,ats,cs);
    1.17  
    1.18 @@ -535,7 +535,7 @@
    1.19  fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
    1.20  let fun xn_list(x,n) =
    1.21          let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1);
    1.22 -        in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end
    1.23 +        in ListPair.map eta_Var (ixs, take (n+1) Ts) end
    1.24      val lhs = list_comb(f,xn_list("X",k-1))
    1.25      val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
    1.26  in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;