1.1 --- a/src/Tools/isac/CalcElements/termC.sml	Mon Dec 30 11:16:00 2019 +0100
     1.2 +++ b/src/Tools/isac/CalcElements/termC.sml	Wed Jan 15 11:47:38 2020 +0100
     1.3 @@ -7,6 +7,10 @@
     1.4  (* TERM_C extends Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *)
     1.5  signature TERM_C =
     1.6    sig
     1.7 +    datatype lrd = D | L | R
     1.8 +    type path
     1.9 +    val path2str: path -> string
    1.10 +
    1.11      val contains_Var: term -> bool
    1.12      val dest_binop_typ: typ -> typ * typ * typ
    1.13      val dest_equals: term -> term * term
    1.14 @@ -97,6 +101,14 @@
    1.15  struct
    1.16  (**)
    1.17  
    1.18 +datatype lrd = L (*t1 in "t1$t2"*)
    1.19 +             | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*)
    1.20 +type path = lrd list; 
    1.21 +fun ldr2str L = "L"
    1.22 +  | ldr2str R = "R"
    1.23 +  | ldr2str D = "D";
    1.24 +fun path2str k = (strs2str' o (map ldr2str)) k;
    1.25 +
    1.26  fun isastr_of_int i = if i >= 0 then string_of_int i else "-" ^ string_of_int (abs i)
    1.27  
    1.28  fun matches thy tm pa =