1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -90,9 +90,6 @@
     1.4    val raise_type_conflicts: term list -> unit
     1.5    val strip_trueprop: term -> term
     1.6  
     1.7 -  val numbers_to_string: term -> term
     1.8 -  val uminus_to_string: term -> term
     1.9 -
    1.10    val var2free: term -> term
    1.11    val vars: term -> term list  (* recognises numerals, should replace "fun vars_of" TODOO*)
    1.12    val vars': term list -> term list
    1.13 @@ -494,9 +491,6 @@
    1.14    end;
    1.15  
    1.16  (** transform binary numeralsstrings **)
    1.17 -val numbers_to_string = ThmC_Def.num_to_Free
    1.18 -val uminus_to_string = ThmC_Def.uminus_to_string
    1.19 -
    1.20  fun mk_Free (s,T) = Free (s, T);
    1.21  fun mk_free T s =  Free (s, T);
    1.22  
    1.23 @@ -542,21 +536,21 @@
    1.24  (* TODO clarify parse with Test_Isac *)
    1.25  fun parseold thy str = (* before 2002 *)
    1.26    \<^try>\<open>
    1.27 -    let val t = ((*typ_a2real o*) numbers_to_string) (Syntax.read_term_global thy str)
    1.28 +    let val t = Syntax.read_term_global thy str
    1.29      in Thm.global_cterm_of thy t end\<close>;
    1.30  fun parseN thy str = (* introduced 2002 *)
    1.31    \<^try>\<open>
    1.32      let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
    1.33      in Thm.global_cterm_of thy t end\<close>;
    1.34  
    1.35 -fun parse_strict thy str = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
    1.36 +fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str);
    1.37  fun parse thy str = (* introduced 2010 *)
    1.38    \<^try>\<open>
    1.39      let val t = parse_strict thy str
    1.40      in Thm.global_cterm_of thy t end\<close>;
    1.41  
    1.42  (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
    1.43 -fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str |> numbers_to_string\<close>;
    1.44 +fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;
    1.45  fun parseNEW' ctxt str = 
    1.46    case parseNEW ctxt str of
    1.47      SOME t => t