1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Thu Oct 20 12:12:18 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Fri Oct 21 15:19:00 2022 +0200
     1.3 @@ -75,9 +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 1.replaced by parse_patt*)
     1.8  (*goal*)val parse: Proof.context -> string -> term
     1.9 -  val parse_patt_PIDE: theory -> string -> term       (*rename to parse_patt*)
    1.10  (*goal*)val parse_patt: theory -> string -> term      (*with typ_a2real still for tests *)
    1.11    (*for test/* *)
    1.12  (*goal*)val parse_test: Proof.context -> string -> term
    1.13 @@ -562,17 +560,12 @@
    1.14  (*\----- old versions to be eliminated -------------------------------------------------------/*)
    1.15  
    1.16  (* to be replaced by parse..*)
    1.17 -fun parse_strict thy str = (*typ_a2real*) (Syntax.read_term_global thy str);
    1.18  fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
    1.19  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
    1.20  (*rename to parse_patt..*)
    1.21 -fun parse_patt_PIDE thy str = (thy, str)
    1.22 -  |>> Proof_Context.init_global
    1.23 -  |-> Proof_Context.read_term_pattern
    1.24  fun parse_patt thy str = (thy, str)
    1.25    |>> Proof_Context.init_global
    1.26    |-> Proof_Context.read_term_pattern
    1.27 -(**)|> typ_a2real;       (** )TODO drop*)
    1.28  
    1.29  (** parse in test/* **)
    1.30  (*