1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jul 13 09:49:45 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jul 13 10:43:21 2021 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val mk_frac: typ -> int * (int * int) -> term
     1.5    val term_of_num: typ -> int -> term
     1.6    val num_of_term: term -> int
     1.7 +  val to_string: term -> string
     1.8    val int_of_str: string -> int
     1.9    val isastr_of_int: int -> string
    1.10    val int_opt_of_string: string -> int option
    1.11 @@ -38,6 +39,7 @@
    1.12    val isapair2pair: term -> term * term (* rename to dest_pair, compare HOLogic.dest_string *)
    1.13  
    1.14    val is_atom: term -> bool
    1.15 +  val string_of_atom: term -> string
    1.16    val is_const: term -> bool
    1.17    val is_variable: term -> bool
    1.18    val is_bdv: string -> bool
    1.19 @@ -273,6 +275,8 @@
    1.20  
    1.21  val term_of_num = HOLogic.mk_number;
    1.22  fun num_of_term t = t |> HOLogic.dest_number |> snd;
    1.23 +(* accomodate string-representation for int to term-orders in Poly.thy and Rational.thy*)
    1.24 +fun to_string t = t |> num_of_term |> LibraryC.string_of_int'
    1.25  
    1.26  fun is_const (Const _) = true | is_const _ = false;
    1.27  fun is_variable (t as Free _) = not (is_num t)
    1.28 @@ -558,6 +562,13 @@
    1.29    | is_atom (Free _) = true
    1.30    | is_atom (Var _) = true
    1.31    | is_atom _ = false;
    1.32 +fun string_of_atom (t as Const ("Num.numeral_class.numeral", _) $ _) = to_string t
    1.33 +  | string_of_atom (t as Const ("Groups.one_class.one", _)) = to_string t
    1.34 +  | string_of_atom (t as Const ("Groups.zero_class.zero", _)) = to_string t
    1.35 +  | string_of_atom (Const (str, _)) = str
    1.36 +  | string_of_atom (Free (str, _)) = str
    1.37 +  | string_of_atom (Var ((str, int), _)) = str ^ "_" ^ string_of_int int
    1.38 +  | string_of_atom _ = "DUMMY-string_of_atom";
    1.39  
    1.40  (* from Pure/term.ML; reports if ALL Free's have found a substitution
    1.41     (required for evaluating the preconditions of _incomplete_ models) *)