1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon Jul 19 18:39:02 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Jul 20 14:37:56 2021 +0200
     1.3 @@ -68,12 +68,9 @@
     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: theory -> string -> cterm option
     1.8 -  val parseN: theory -> string -> cterm option
     1.9    val parseNEW: Proof.context -> string -> term option
    1.10    val parseNEW': Proof.context -> string -> term
    1.11    val parseNEW'': theory -> string -> term
    1.12 -  val parseold: theory -> string -> cterm option
    1.13    val parse_strict: theory -> string -> term
    1.14    val parse_patt: theory -> string -> term
    1.15    val perm: term -> term -> bool
    1.16 @@ -533,21 +530,21 @@
    1.17    | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
    1.18    | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
    1.19  
    1.20 -(* TODO clarify parse with Test_Isac *)
    1.21 +(* TODO clarify parse with Test_Isac * )
    1.22  fun parseold thy str = (* before 2002 *)
    1.23    \<^try>\<open>
    1.24      let val t = Syntax.read_term_global thy str
    1.25      in Thm.global_cterm_of thy t end\<close>;
    1.26  fun parseN thy str = (* introduced 2002 *)
    1.27    \<^try>\<open>
    1.28 -    let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
    1.29 +    let val t = Syntax.read_term_global thy str
    1.30      in Thm.global_cterm_of thy t end\<close>;
    1.31  
    1.32 -fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str);
    1.33  fun parse thy str = (* introduced 2010 *)
    1.34    \<^try>\<open>
    1.35      let val t = parse_strict thy str
    1.36      in Thm.global_cterm_of thy t end\<close>;
    1.37 +*)
    1.38  
    1.39  (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
    1.40  fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;
    1.41 @@ -559,6 +556,7 @@
    1.42    case parseNEW (ThyC.to_ctxt thy) str of
    1.43      SOME t => t
    1.44    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    1.45 +fun parse_strict thy str = (*typ_a2real*) (parseNEW'' thy str);
    1.46  
    1.47  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
    1.48    WN130613 probably compare to