diff -r 820bf0840029 -r 995177b6d786 src/Tools/isac/BaseDefinitions/termC.sml
--- a/src/Tools/isac/BaseDefinitions/termC.sml	Tue Apr 14 12:39:26 2020 +0200
+++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Apr 14 15:56:15 2020 +0200
@@ -28,9 +28,9 @@
 
   val term_of_num: typ -> int -> term
   val num_of_term: term -> int
-  val int_of_str_opt: string -> int option
   val int_of_str: string -> int
   val isastr_of_int: int -> string
+  val int_opt_of_string: string -> int option  (* belongs to TermC *)
 
   val isalist2list: term -> term list
   val list2isalist: typ -> term list -> term
@@ -235,13 +235,13 @@
   else string_of_int n;
 val int_of_str = Value.parse_int;
 
-val int_of_str_opt = ThmC_Def.int_of_str_opt
+val int_opt_of_string = ThmC_Def.int_opt_of_string
 
-fun is_num' str = case int_of_str_opt str of SOME _ => true | NONE => false;
+fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
 fun is_num (Free (s, _)) = if is_num' s then true else false | is_num _ = false;
 fun term_of_num ntyp n = Free (str_of_int n, ntyp);
 fun num_of_term (t as (Free (istr, _))) = 
-    (case int_of_str_opt istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
+    (case int_opt_of_string istr of SOME i => i | NONE => raise TERM ("num_of_term: NOT int ", [t]))
   | num_of_term t = raise TERM ("num_of_term: NOT Free ", [t])
 
 fun is_const (Const _) = true | is_const _ = false;
@@ -437,7 +437,7 @@
   end;
 
 (** transform binary numeralsstrings **)
-val numbers_to_string = ThmC_Def.numbers_to_string
+val numbers_to_string = ThmC_Def.num_to_Free
 val uminus_to_string = ThmC_Def.uminus_to_string
 
 fun mk_Free (s,T) = Free (s, T);
@@ -507,11 +507,11 @@
 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
   WN130613 probably compare to 
   http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
-fun parse_patt thy str =
-  (thy, str) |>> ThyC.thy2ctxt 
-             |-> Proof_Context.read_term_pattern
-             |> numbers_to_string (*TODO drop*)
-             |> typ_a2real;       (*TODO drop*)
+fun parse_patt thy str = (thy, str)
+  |>> ThyC.thy2ctxt 
+  |-> Proof_Context.read_term_pattern
+  |> numbers_to_string (*TODO drop*)
+  |> typ_a2real;       (*TODO drop*)
 fun str2term str = parse_patt (ThyC.Thy_Info_get_theory "Isac_Knowledge") str
 
 (* TODO decide with Test_Isac *)