1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jul 13 15:28:43 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Thu Jul 15 14:10:18 2021 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    val inst_bdv: (term * term) list -> term -> term
     1.5  
     1.6    val mk_frac: typ -> int * (int * int) -> term
     1.7 +  val numerals_to_Free: term -> term
     1.8    val term_of_num: typ -> int -> term
     1.9    val num_of_term: term -> int
    1.10    val to_string: term -> string
    1.11 @@ -273,9 +274,21 @@
    1.12      else Const ("Rings.divide_class.divide", T --> T --> T) $
    1.13        mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2
    1.14  
    1.15 +val numerals_to_Free = (* Makarius 100308 *)
    1.16 +  let
    1.17 +    fun dest_num t =
    1.18 +      (case try HOLogic.dest_number t of
    1.19 +        SOME (T, i) => SOME (Free (signed_string_of_int i, T))
    1.20 +      | NONE => NONE);
    1.21 +    fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
    1.22 +      | to_str (t as (u1 $ u2)) =
    1.23 +          (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
    1.24 +      | to_str t = perhaps dest_num t;
    1.25 +  in to_str end
    1.26 +
    1.27  val term_of_num = HOLogic.mk_number;
    1.28  fun num_of_term t = t |> HOLogic.dest_number |> snd;
    1.29 -(* accomodate string-representation for int to term-orders in Poly.thy and Rational.thy*)
    1.30 +(* accomodate string-representation for int to term-orders *)
    1.31  fun to_string t = t |> num_of_term |> LibraryC.string_of_int'
    1.32  
    1.33  fun is_const (Const _) = true | is_const _ = false;