1.1 --- a/src/Tools/isac/CalcElements/calcelems.sml	Wed Nov 06 15:08:27 2019 +0100
     1.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml	Wed Nov 06 18:34:29 2019 +0100
     1.3 @@ -62,8 +62,8 @@
     1.4      val trace_rewrite: bool Unsynchronized.ref
     1.5      val depth: int Unsynchronized.ref
     1.6      val assoc_thy: Rule.theory' -> theory
     1.7 -    type loc_
     1.8 -    val loc_2str: loc_ -> string
     1.9 +    type path
    1.10 +    val path2str: path -> string
    1.11      type thm''
    1.12      val metID2str: string list -> string
    1.13      val e_pblID: pblID
    1.14 @@ -96,7 +96,7 @@
    1.15      val ketype2str': ketype -> string
    1.16      val str2ketype': string -> ketype
    1.17      val thmID_of_derivation_name': thm -> string
    1.18 -    eqtype path
    1.19 +    eqtype filepath
    1.20      val theID2thyID: theID -> Rule.thyID
    1.21      val thy2guh: theID -> guh
    1.22      val thypart2guh: theID -> guh
    1.23 @@ -400,7 +400,7 @@
    1.24      | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
    1.25    | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
    1.26  
    1.27 -type path = string;
    1.28 +type filepath = string;
    1.29  type filename = string;
    1.30  
    1.31  
    1.32 @@ -463,15 +463,13 @@
    1.33  val check_guhs_unique = Unsynchronized.ref true;
    1.34  
    1.35  
    1.36 -datatype lrd = (*elements of "type loc_" into an Isabelle term*)
    1.37 -	L   (*go left at $*)
    1.38 -| R   (*go right at $*)
    1.39 -| D;  (*go down at Abs*)
    1.40 -type loc_ = lrd list;
    1.41 +datatype lrd = L (*t1 in "t1$t2"*)
    1.42 +             | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*)
    1.43 +type path = lrd list; 
    1.44  fun ldr2str L = "L"
    1.45    | ldr2str R = "R"
    1.46    | ldr2str D = "D";
    1.47 -fun loc_2str k = (strs2str' o (map ldr2str)) k;
    1.48 +fun path2str k = (strs2str' o (map ldr2str)) k;
    1.49  
    1.50  
    1.51  (* the pattern for an item of a problems model or a methods guard *)