diff -r 9529c8483d00 -r 815b0dc8b589 src/Tools/isac/BaseDefinitions/termC.sml
--- a/src/Tools/isac/BaseDefinitions/termC.sml	Sat Jun 12 18:33:15 2021 +0200
+++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jun 15 22:24:20 2021 +0200
@@ -63,6 +63,7 @@
   val mk_var_op_num: term -> string -> typ -> typ -> int -> term
 
   val matches: theory -> term -> term -> bool
+  val parse_strict: theory -> string -> term
   val parse: theory -> string -> cterm option
   val parseN: theory -> string -> cterm option
   val parseNEW: Proof.context -> string -> term option
@@ -504,9 +505,11 @@
   \<^try>\<open>
     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 o numbers_to_string) (Syntax.read_term_global thy str);
 fun parse thy str = (* introduced 2010 *)
   \<^try>\<open>
-    let val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str)
+    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*)