1.1 --- a/src/Provers/eqsubst.ML	Mon May 21 19:11:42 2007 +0200
     1.2 +++ b/src/Provers/eqsubst.ML	Mon May 21 19:13:38 2007 +0200
     1.3 @@ -106,7 +106,8 @@
     1.4         searchinfo -> Term.term -> match Seq.seq Seq.seq
     1.5      val searchf_lr_unify_valid :
     1.6         searchinfo -> Term.term -> match Seq.seq Seq.seq
     1.7 -
     1.8 +    val searchf_bt_unify_valid :
     1.9 +       searchinfo -> Term.term -> match Seq.seq Seq.seq
    1.10  
    1.11      (* syntax tools *)
    1.12      val ith_syntax : Args.T list -> int list * Args.T list
    1.13 @@ -313,16 +314,34 @@
    1.14            end;
    1.15      in Z.lzy_search sf_valid_td_lr end;
    1.16  
    1.17 +(* search from bottom to top, left to right *)
    1.18 +
    1.19 +fun search_bt_valid validf =
    1.20 +    let 
    1.21 +      fun sf_valid_td_lr z = 
    1.22 +          let val here = if validf z then [Z.Here z] else [] in
    1.23 +            case Z.trm z 
    1.24 +             of _ $ _ => [Z.LookIn (Z.move_down_left z), 
    1.25 +                          Z.LookIn (Z.move_down_right z)] @ here
    1.26 +              | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
    1.27 +              | _ => here
    1.28 +          end;
    1.29 +    in Z.lzy_search sf_valid_td_lr end;
    1.30 +
    1.31 +fun searchf_unify_gen f (sgn, maxidx, z) lhs =
    1.32 +    Seq.map (clean_unify_z sgn maxidx lhs) 
    1.33 +            (Z.limit_apply f z);
    1.34 +
    1.35  (* search all unifications *)
    1.36 -fun searchf_lr_unify_all (sgn, maxidx, z) lhs =
    1.37 -    Seq.map (clean_unify_z sgn maxidx lhs) 
    1.38 -            (Z.limit_apply search_lr_all z);
    1.39 +val searchf_lr_unify_all =
    1.40 +    searchf_unify_gen search_lr_all;
    1.41  
    1.42  (* search only for 'valid' unifiers (non abs subterms and non vars) *)
    1.43 -fun searchf_lr_unify_valid (sgn, maxidx, z) lhs  =
    1.44 -    Seq.map (clean_unify_z sgn maxidx lhs) 
    1.45 -            (Z.limit_apply (search_lr_valid valid_match_start) z);
    1.46 +val searchf_lr_unify_valid = 
    1.47 +    searchf_unify_gen (search_lr_valid valid_match_start);
    1.48  
    1.49 +val searchf_bt_unify_valid =
    1.50 +    searchf_unify_gen (search_bt_valid valid_match_start);
    1.51  
    1.52  (* apply a substitution in the conclusion of the theorem th *)
    1.53  (* cfvs are certified free var placeholders for goal params *)