diff -r da7dd260f66e -r 6e63e5fe3e7d src/Tools/isac/BaseDefinitions/termC.sml
--- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon Oct 31 16:43:48 2022 +0100
+++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Oct 31 16:53:59 2022 +0100
@@ -76,7 +76,7 @@
   val parseNEW': Proof.context -> string -> term      (*old version to be eliminated*)
   val parseNEW'': theory -> string -> term            (*old version to be eliminated*)
 (*goal*)val parse: Proof.context -> string -> term
-(*goal*)val parse_patt: theory -> string -> term      (*with typ_a2real still for tests *)
+(*goal*)val parse_patt: theory -> string -> term
   (*for test/* *)
 (*goal*)val parse_test: Proof.context -> string -> term
 (*goal*)val parse_patt_test: theory -> string -> term
@@ -527,23 +527,6 @@
   | inst_abs (t1 $ t2) = inst_abs t1 $ inst_abs t2
   | inst_abs t = t;
 
-(* for parse and parse_patt: fix all types to real *)
-fun T_a2real (Type (s, [])) = 
-    if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])
-  | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)
-  | T_a2real (TFree (s, srt)) = 
-    if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)
-  | T_a2real (TVar (("DUMMY", _), _)) = HOLogic.realT
-  | T_a2real (TVar ((s, i), srt)) = 
-    if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TVar ((s, i), srt)
-(*val typ_a2real: term -> term*)
-fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T)) 
-  | typ_a2real (Free( s, T)) = (Free( s, T_a2real T))
-  | typ_a2real (Var( n, T)) = (Var( n, T_a2real T))
-  | typ_a2real (Bound i) = (Bound i)
-  | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
-  | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
-
 
 (*** parse ***)
 
@@ -562,7 +545,6 @@
 (* to be replaced by parse..*)
 fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
-(*rename to parse_patt..*)
 fun parse_patt thy str = (thy, str)
   |>> Proof_Context.init_global
   |-> Proof_Context.read_term_pattern