src/Provers/eqsubst.ML
changeset 19861 620d90091788
parent 19835 81d6dc597559
child 19871 88e8f6173bab
     1.1 --- a/src/Provers/eqsubst.ML	Mon Jun 12 21:18:10 2006 +0200
     1.2 +++ b/src/Provers/eqsubst.ML	Mon Jun 12 21:19:00 2006 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4               Envir.alist_of env);
     1.5            val initenv = Envir.Envir {asol = Vartab.empty,
     1.6                                       iTs = typinsttab, maxidx = ix2};
     1.7 -          val useq = (Unify.smash_unifiers (sgn,initenv,[a]))
     1.8 +          val useq = Unify.smash_unifiers sgn [a] initenv
     1.9  	            handle UnequalLengths => Seq.empty
    1.10  		               | Term.TERM _ => Seq.empty;
    1.11            fun clean_unify' useq () =
    1.12 @@ -380,9 +380,8 @@
    1.13                  (case searchf searchinfo occ lhs of
    1.14                     SkipMore i => occ_search i moreasms
    1.15                   | SkipSeq ss =>
    1.16 -                   Seq.append (Seq.map (Library.pair asminfo)
    1.17 -                                       (Seq.flat ss),
    1.18 -                               occ_search 1 moreasms))
    1.19 +                   Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
    1.20 +                               (occ_search 1 moreasms))
    1.21                                (* find later substs also *)
    1.22            in
    1.23              occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)