diff -r 0d22a6bf1fc6 -r 0ee698b0a703 src/Tools/isac/BaseDefinitions/termC.sml
--- a/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jul 20 14:37:56 2021 +0200
+++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jul 27 11:21:14 2021 +0200
@@ -68,9 +68,12 @@
   val mk_var_op_num: term -> string -> typ -> typ -> int -> term
 
   val matches: theory -> term -> term -> bool
+  val parse: theory -> string -> cterm option
+  val parseN: theory -> string -> cterm option
   val parseNEW: Proof.context -> string -> term option
   val parseNEW': Proof.context -> string -> term
   val parseNEW'': theory -> string -> term
+  val parseold: theory -> string -> cterm option
   val parse_strict: theory -> string -> term
   val parse_patt: theory -> string -> term
   val perm: term -> term -> bool
@@ -530,21 +533,21 @@
   | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
   | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
 
-(* TODO clarify parse with Test_Isac * )
+(* TODO clarify parse with Test_Isac *)
 fun parseold thy str = (* before 2002 *)
   \<^try>\<open>
     let val t = Syntax.read_term_global thy str
     in Thm.global_cterm_of thy t end\<close>;
 fun parseN thy str = (* introduced 2002 *)
   \<^try>\<open>
-    let val t = Syntax.read_term_global thy str
+    let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
     in Thm.global_cterm_of thy t end\<close>;
 
+fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str);
 fun parse thy str = (* introduced 2010 *)
   \<^try>\<open>
     let val t = parse_strict thy str
     in Thm.global_cterm_of thy t end\<close>;
-*)
 
 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
 fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;
@@ -556,7 +559,6 @@
   case parseNEW (ThyC.to_ctxt thy) str of
     SOME t => t
   | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
-fun parse_strict thy str = (*typ_a2real*) (parseNEW'' thy str);
 
 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
   WN130613 probably compare to