diff -r b25aaadac5f3 -r 96355a86c11e src/Tools/isac/BaseDefinitions/termC.sml
--- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Sep 29 18:56:38 2021 +0200
+++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Sep 29 19:26:12 2021 +0200
@@ -74,7 +74,6 @@
   val parseNEW: Proof.context -> string -> term option
   val parseNEW': Proof.context -> string -> term
   val parseNEW'': theory -> string -> term
-  val parseold: theory -> string -> cterm option
   val parseN: theory -> string -> cterm option
   val parse_strict: theory -> string -> term
   val parse: theory -> string -> cterm option
@@ -557,10 +556,6 @@
   | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
 
 (* TODO clarify parse with Test_Isac *)
-fun parseold thy str = (* before 2002 *)
-  \<^try>\<open>
-    let val t = Syntax.read_term_global thy str
-    in Thm.global_cterm_of thy t end\<close>;
 fun parseN thy str = (* introduced 2002 *)
   \<^try>\<open>
     let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)