1.1 --- a/src/Tools/isac/CalcElements/termC.sml	Wed Jan 15 11:47:38 2020 +0100
     1.2 +++ b/src/Tools/isac/CalcElements/termC.sml	Wed Jan 15 12:01:13 2020 +0100
     1.3 @@ -10,6 +10,8 @@
     1.4      datatype lrd = D | L | R
     1.5      type path
     1.6      val path2str: path -> string
     1.7 +    val at_location: path -> term -> term
     1.8 +    val go_up: path -> term -> term
     1.9  
    1.10      val contains_Var: term -> bool
    1.11      val dest_binop_typ: typ -> typ * typ * typ
    1.12 @@ -108,6 +110,14 @@
    1.13    | ldr2str R = "R"
    1.14    | ldr2str D = "D";
    1.15  fun path2str k = (strs2str' o (map ldr2str)) k;
    1.16 +(*go to a location in a term and fetch the resective sub-term*)
    1.17 +fun at_location [] t = t
    1.18 +  | at_location (D :: p) (Abs(_, _, body)) = at_location (p : path) body
    1.19 +  | at_location (L :: p) (t1 $ _) = at_location p t1
    1.20 +  | at_location (R :: p) (_ $ t2) = at_location p t2
    1.21 +  | at_location l _ = error ("at_location: no " ^ path2str l);
    1.22 +fun go_up l t =
    1.23 +  if length l > 1 then at_location (drop_last l) t else raise ERROR ("go_up [] " ^ Rule.term2str t)
    1.24  
    1.25  fun isastr_of_int i = if i >= 0 then string_of_int i else "-" ^ string_of_int (abs i)
    1.26