1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Thu Oct 20 10:47:52 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Thu Oct 20 12:12:18 2022 +0200
     1.3 @@ -75,8 +75,7 @@
     1.4    val parseNEW: Proof.context -> string -> term option(*old version to be eliminated*)
     1.5    val parseNEW': Proof.context -> string -> term      (*old version to be eliminated*)
     1.6    val parseNEW'': theory -> string -> term            (*old version to be eliminated*)
     1.7 -  val parse_strict: theory -> string -> term          (*to be replaced by parse, typ_a2real for CAS_Cmd*)
     1.8 -  val parse_strict_PIDE: theory -> string -> term     (*to be 1.replaced by parse_patt*)
     1.9 +  val parse_strict: theory -> string -> term     (*to be 1.replaced by parse_patt*)
    1.10  (*goal*)val parse: Proof.context -> string -> term
    1.11    val parse_patt_PIDE: theory -> string -> term       (*rename to parse_patt*)
    1.12  (*goal*)val parse_patt: theory -> string -> term      (*with typ_a2real still for tests *)
    1.13 @@ -562,10 +561,8 @@
    1.14    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    1.15  (*\----- old versions to be eliminated -------------------------------------------------------/*)
    1.16  
    1.17 -(* to be replaced by parse-test..*)
    1.18 -fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str); (*still for CAS_Cmd*)
    1.19  (* to be replaced by parse..*)
    1.20 -fun parse_strict_PIDE thy str = (*typ_a2real*) (Syntax.read_term_global thy str);
    1.21 +fun parse_strict thy str = (*typ_a2real*) (Syntax.read_term_global thy str);
    1.22  fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
    1.23  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
    1.24  (*rename to parse_patt..*)