1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Fri May 27 15:12:54 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Fri May 27 17:14:49 2022 +0200
     1.3 @@ -75,7 +75,6 @@
     1.4    val parseNEW': Proof.context -> string -> term
     1.5    val parseNEW'': theory -> string -> term
     1.6    val parse_strict: theory -> string -> term
     1.7 -(*val parse: theory -> string -> cterm option*)
     1.8  
     1.9    val parse_patt: theory -> string -> term
    1.10    val perm: term -> term -> bool
    1.11 @@ -556,10 +555,6 @@
    1.12  
    1.13  (* TODO clarify parse with Test_Isac *)
    1.14  fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str);
    1.15 -fun parse thy str = (* introduced 2010 *)
    1.16 -  \<^try>\<open>
    1.17 -    let val t = parse_strict thy str
    1.18 -    in Thm.global_cterm_of thy t end\<close>;
    1.19  
    1.20  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
    1.21    WN130613 probably compare to