2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
15 (* Internal functions *******************************************************)
17 let rec lref_map_bind f map b = match b with
19 let f v' = f (S.sh1 v v' b B.abbr) in
22 let f w' = f (S.sh1 w w' b B.abst) in
26 and lref_map f map t = match t with
28 let ii = map i in f (S.sh1 i ii t B.lref)
32 let f w' u' = f (S.sh2 w w' u u' t B.cast) in
33 let f w' = lref_map (f w') map u in
36 let f w' u' = f (S.sh2 w w' u u' t B.appl) in
37 let f w' = lref_map (f w') map u in
39 | B.Bind (l, id, b, u) ->
40 let f b' u' = f (S.sh2 b b' u u' t (B.bind l id)) in
41 let f b' = lref_map (f b') map u in
44 (* Interface functions ******************************************************)
46 let subst f new_l old_l t =
47 let map i = if i = old_l then new_l else i in
48 if new_l = old_l then f t else lref_map f map t