1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sat Jun 12 18:33:15 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jun 15 22:24:20 2021 +0200
     1.3 @@ -63,6 +63,7 @@
     1.4    val mk_var_op_num: term -> string -> typ -> typ -> int -> term
     1.5  
     1.6    val matches: theory -> term -> term -> bool
     1.7 +  val parse_strict: theory -> string -> term
     1.8    val parse: theory -> string -> cterm option
     1.9    val parseN: theory -> string -> cterm option
    1.10    val parseNEW: Proof.context -> string -> term option
    1.11 @@ -504,9 +505,11 @@
    1.12    \<^try>\<open>
    1.13      let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
    1.14      in Thm.global_cterm_of thy t end\<close>;
    1.15 +
    1.16 +fun parse_strict thy str = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
    1.17  fun parse thy str = (* introduced 2010 *)
    1.18    \<^try>\<open>
    1.19 -    let val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str)
    1.20 +    let val t = parse_strict thy str
    1.21      in Thm.global_cterm_of thy t end\<close>;
    1.22  
    1.23  (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)