1.1 --- a/src/Tools/eqsubst.ML	Wed Dec 15 15:01:34 2010 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Wed Dec 15 15:11:56 2010 +0100
     1.3 @@ -119,11 +119,8 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -structure EqSubst
     1.8 -: EQSUBST
     1.9 -= struct
    1.10 -
    1.11 -structure Z = Zipper;
    1.12 +structure EqSubst: EQSUBST =
    1.13 +struct
    1.14  
    1.15  (* changes object "=" to meta "==" which prepares a given rewrite rule *)
    1.16  fun prep_meta_eq ctxt =
    1.17 @@ -196,11 +193,11 @@
    1.18  abstracted out) for use in rewriting with RWInst.rw *)
    1.19  fun prep_zipper_match z = 
    1.20      let 
    1.21 -      val t = Z.trm z  
    1.22 -      val c = Z.ctxt z
    1.23 -      val Ts = Z.C.nty_ctxt c
    1.24 +      val t = Zipper.trm z  
    1.25 +      val c = Zipper.ctxt z
    1.26 +      val Ts = Zipper.C.nty_ctxt c
    1.27        val (FakeTs', Ts', t') = fakefree_badbounds Ts t
    1.28 -      val absterm = mk_foo_match (Z.C.apply c) Ts' t'
    1.29 +      val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
    1.30      in
    1.31        (t', (FakeTs', Ts', absterm))
    1.32      end;
    1.33 @@ -291,7 +288,7 @@
    1.34  (* Avoid considering replacing terms which have a var at the head as
    1.35     they always succeed trivially, and uninterestingly. *)
    1.36  fun valid_match_start z =
    1.37 -    (case bot_left_leaf_of (Z.trm z) of 
    1.38 +    (case bot_left_leaf_of (Zipper.trm z) of 
    1.39        Var _ => false 
    1.40        | _ => true);
    1.41  
    1.42 @@ -302,33 +299,33 @@
    1.43  fun search_lr_valid validf =
    1.44      let 
    1.45        fun sf_valid_td_lr z = 
    1.46 -          let val here = if validf z then [Z.Here z] else [] in
    1.47 -            case Z.trm z 
    1.48 -             of _ $ _ => [Z.LookIn (Z.move_down_left z)] 
    1.49 +          let val here = if validf z then [Zipper.Here z] else [] in
    1.50 +            case Zipper.trm z 
    1.51 +             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)] 
    1.52                           @ here 
    1.53 -                         @ [Z.LookIn (Z.move_down_right z)]
    1.54 -              | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
    1.55 +                         @ [Zipper.LookIn (Zipper.move_down_right z)]
    1.56 +              | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
    1.57                | _ => here
    1.58            end;
    1.59 -    in Z.lzy_search sf_valid_td_lr end;
    1.60 +    in Zipper.lzy_search sf_valid_td_lr end;
    1.61  
    1.62  (* search from bottom to top, left to right *)
    1.63  
    1.64  fun search_bt_valid validf =
    1.65      let 
    1.66        fun sf_valid_td_lr z = 
    1.67 -          let val here = if validf z then [Z.Here z] else [] in
    1.68 -            case Z.trm z 
    1.69 -             of _ $ _ => [Z.LookIn (Z.move_down_left z), 
    1.70 -                          Z.LookIn (Z.move_down_right z)] @ here
    1.71 -              | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
    1.72 +          let val here = if validf z then [Zipper.Here z] else [] in
    1.73 +            case Zipper.trm z 
    1.74 +             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z), 
    1.75 +                          Zipper.LookIn (Zipper.move_down_right z)] @ here
    1.76 +              | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
    1.77                | _ => here
    1.78            end;
    1.79 -    in Z.lzy_search sf_valid_td_lr end;
    1.80 +    in Zipper.lzy_search sf_valid_td_lr end;
    1.81  
    1.82  fun searchf_unify_gen f (sgn, maxidx, z) lhs =
    1.83      Seq.map (clean_unify_z sgn maxidx lhs) 
    1.84 -            (Z.limit_apply f z);
    1.85 +            (Zipper.limit_apply f z);
    1.86  
    1.87  (* search all unifications *)
    1.88  val searchf_lr_unify_all =
    1.89 @@ -369,9 +366,9 @@
    1.90        val conclterm = Logic.strip_imp_concl fixedbody;
    1.91        val conclthm = trivify conclterm;
    1.92        val maxidx = Thm.maxidx_of th;
    1.93 -      val ft = ((Z.move_down_right (* ==> *)
    1.94 -                 o Z.move_down_left (* Trueprop *)
    1.95 -                 o Z.mktop
    1.96 +      val ft = ((Zipper.move_down_right (* ==> *)
    1.97 +                 o Zipper.move_down_left (* Trueprop *)
    1.98 +                 o Zipper.mktop
    1.99                   o Thm.prop_of) conclthm)
   1.100      in
   1.101        ((cfvs, conclthm), (sgn, maxidx, ft))
   1.102 @@ -487,8 +484,8 @@
   1.103        val pth = trivify asmt;
   1.104        val maxidx = Thm.maxidx_of th;
   1.105  
   1.106 -      val ft = ((Z.move_down_right (* trueprop *)
   1.107 -                 o Z.mktop
   1.108 +      val ft = ((Zipper.move_down_right (* trueprop *)
   1.109 +                 o Zipper.mktop
   1.110                   o Thm.prop_of) pth)
   1.111      in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   1.112