1.1 --- a/src/Tools/isac/BaseDefinitions/libraryC.sml	Tue Aug 17 22:39:48 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/libraryC.sml	Tue Aug 17 22:50:20 2021 +0200
     1.3 @@ -61,7 +61,6 @@
     1.4    val pair2tri: ('a * 'b) * 'c -> 'a * 'b * 'c
     1.5    val snd3: 'a * 'b * 'c -> 'b
     1.6    val spair2str: string * string -> string
     1.7 -  val string_of_int': int -> string
     1.8  
     1.9    val split_nlast: int * 'a list -> 'a list * 'a list
    1.10    val string_to_bool: string -> bool
    1.11 @@ -176,10 +175,6 @@
    1.12  fun spair2str (s1, s2) =   "(" ^ quote s1  ^ ", " ^ quote s2 ^ ")";
    1.13  fun pair2str_ (s1, s2) =   s1 ^ "#" ^ s2;
    1.14  fun pair2str (s1, s2) =   "(" ^ s1 ^ ", " ^ s2 ^ ")";
    1.15 -(* accomodate string-representation for int to term-orders in Poly.thy and Rational.thy*)
    1.16 -fun string_of_int' i =
    1.17 -    if i >= 0 then i |> string_of_int
    1.18 -    else (i * ~1) |> string_of_int |> curry op ^ "-"
    1.19  
    1.20  val int2str = Library.string_of_int;
    1.21  fun ints2str' ints = (strs2str' o (map string_of_int)) ints;

     2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Tue Aug 17 22:39:48 2021 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Aug 17 22:50:20 2021 +0200
     2.3 @@ -288,7 +288,7 @@
     2.4  val term_of_num = HOLogic.mk_number;
     2.5  fun num_of_term t = t |> HOLogic.dest_number |> snd;
     2.6  (* accomodate string-representation for int to term-orders *)
     2.7 -fun to_string t = t |> num_of_term |> LibraryC.string_of_int'
     2.8 +fun to_string t = t |> num_of_term |> signed_string_of_int
     2.9  
    2.10  fun is_const (Const _) = true | is_const _ = false;
    2.11  fun is_variable (t as Free _) = not (is_num t)