src/FOLP/simp.ML
changeset 42364 8c674b3b8e44
parent 42284 326f57825e1a
child 44121 44adaa6db327
     1.1 --- a/src/FOLP/simp.ML	Sat Apr 16 16:37:21 2011 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sat Apr 16 18:11:20 2011 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4            biresolve_tac (Net.unify_term net
     1.5                         (lhs_of (Logic.strip_assums_concl prem))) i);
     1.6  
     1.7 -fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
     1.8 +fun nth_subgoal i thm = nth (prems_of thm) (i - 1);
     1.9  
    1.10  fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm);
    1.11  
    1.12 @@ -422,7 +422,7 @@
    1.13                      let val ps = prems_of thm
    1.14                          and ps' = prems_of thm';
    1.15                          val n = length(ps')-length(ps);
    1.16 -                        val a = length(Logic.strip_assums_hyp(List.nth(ps,i-1)))
    1.17 +                        val a = length(Logic.strip_assums_hyp(nth ps (i - 1)))
    1.18                          val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps'));
    1.19                      in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
    1.20            | NONE => (REW::ss,thm,anet,ats,cs);