1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Aug 22 11:42:55 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Sun Aug 22 14:28:38 2021 +0200
     1.3 @@ -26,6 +26,9 @@
     1.4    val inst_abs: term -> term
     1.5    val inst_bdv: (term * term) list -> term -> term
     1.6  
     1.7 +  val lhs: term -> term
     1.8 +  val rhs: term -> term
     1.9 +
    1.10    val mk_frac: typ -> int * (int * int) -> term
    1.11    val numerals_to_Free: term -> term
    1.12    val term_of_num: typ -> int -> term
    1.13 @@ -261,6 +264,13 @@
    1.14  
    1.15  fun string_of_num n = (n |> HOLogic.dest_number |> snd |> string_of_int)
    1.16  
    1.17 +(* refer to Thm.lhs_of *)
    1.18 +fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
    1.19 +  | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
    1.20 +fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
    1.21 +  | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");
    1.22 +
    1.23 +
    1.24  fun mk_negative T t = Const (\<^const_name>\<open>uminus\<close>, T --> T) $ t
    1.25  fun mk_frac T (sg, (i1, i2)) =
    1.26    if sg = 1 then