1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Sep 29 18:56:38 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Sep 29 19:26:12 2021 +0200
     1.3 @@ -74,7 +74,6 @@
     1.4    val parseNEW: Proof.context -> string -> term option
     1.5    val parseNEW': Proof.context -> string -> term
     1.6    val parseNEW'': theory -> string -> term
     1.7 -  val parseold: theory -> string -> cterm option
     1.8    val parseN: theory -> string -> cterm option
     1.9    val parse_strict: theory -> string -> term
    1.10    val parse: theory -> string -> cterm option
    1.11 @@ -557,10 +556,6 @@
    1.12    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    1.13  
    1.14  (* TODO clarify parse with Test_Isac *)
    1.15 -fun parseold thy str = (* before 2002 *)
    1.16 -  \<^try>\<open>
    1.17 -    let val t = Syntax.read_term_global thy str
    1.18 -    in Thm.global_cterm_of thy t end\<close>;
    1.19  fun parseN thy str = (* introduced 2002 *)
    1.20    \<^try>\<open>
    1.21      let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)