1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jun 29 15:43:35 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jun 29 16:01:01 2020 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    datatype lrd = D | L | R
     1.5    type path
     1.6    val string_of_path: path -> string
     1.7 -  val at_location: path -> term -> term
     1.8 +  val sub_at: path -> term -> term
     1.9    val go_up: path -> term -> term
    1.10  
    1.11    val contains_Var: term -> bool
    1.12 @@ -130,13 +130,13 @@
    1.13    | ldr2str D = "D";
    1.14  fun string_of_path k = (strs2str' o (map ldr2str)) k;
    1.15  (*go to a location in a term and fetch the resective sub-term*)
    1.16 -fun at_location [] t = t
    1.17 -  | at_location (D :: p) (Abs(_, _, body)) = at_location p body
    1.18 -  | at_location (L :: p) (t1 $ _) = at_location p t1
    1.19 -  | at_location (R :: p) (_ $ t2) = at_location p t2
    1.20 -  | at_location l t = raise TERM ("at_location: no " ^ string_of_path l ^ " for ", [t]);
    1.21 +fun sub_at [] t = t
    1.22 +  | sub_at (D :: p) (Abs(_, _, body)) = sub_at p body
    1.23 +  | sub_at (L :: p) (t1 $ _) = sub_at p t1
    1.24 +  | sub_at (R :: p) (_ $ t2) = sub_at p t2
    1.25 +  | sub_at l t = raise TERM ("sub_at: no " ^ string_of_path l ^ " for ", [t]);
    1.26  fun go_up l t =
    1.27 -  if length l > 1 then at_location (drop_last l) t else raise ERROR ("go_up [] " ^ UnparseC.term t)
    1.28 +  if length l > 1 then sub_at (drop_last l) t else raise ERROR ("go_up [] " ^ UnparseC.term t)
    1.29  
    1.30  fun isastr_of_int i = if i >= 0 then string_of_int i else "-" ^ string_of_int (abs i)
    1.31