1.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml	Mon Apr 13 15:31:23 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml	Mon Apr 13 18:32:01 2020 +0200
     1.3 @@ -109,23 +109,18 @@
     1.4      case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE
     1.5    end;
     1.6  
     1.7 -(** transform binary numeralsstrings **)
     1.8 +(** transform binary numerals to "Free (string, T)" **)
     1.9  
    1.10 -(*Makarius 100308, hacked by WN*)
    1.11 +(* Makarius 100308 *)
    1.12  val numbers_to_string =
    1.13    let
    1.14      fun dest_num t =
    1.15        (case try HOLogic.dest_number t of
    1.16 -        SOME (T, i) =>
    1.17 -          (*if T = @{typ int} orelse T = @{typ real} then WN*)
    1.18 -            SOME (Free (signed_string_of_int i, T))
    1.19 -          (*else NONE  WN*)
    1.20 +        SOME (T, i) => SOME (Free (signed_string_of_int i, T))
    1.21        | NONE => NONE);
    1.22      fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
    1.23        | to_str (t as (u1 $ u2)) =
    1.24 -          (case dest_num t of
    1.25 -            SOME t' => t'
    1.26 -          | NONE => to_str u1 $ to_str u2)
    1.27 +          (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
    1.28        | to_str t = perhaps dest_num t;
    1.29    in to_str end
    1.30  val uminus_to_string =