diff -r b2ff1902420f -r 06ec8abfd3bc src/Tools/isac/BaseDefinitions/termC.sml
--- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 09:23:18 2023 +0100
+++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Jan 11 11:38:01 2023 +0100
@@ -85,7 +85,6 @@
   val str_of_int: int -> string
   val strip_imp_prems': term -> term option
   val subst_atomic_all: LibraryC.subst -> term -> bool * term
-  val term_detail2str: term -> string
 
   val pairt: term -> term -> term
   val pairT: typ -> typ -> typ
@@ -103,19 +102,19 @@
   val contains_Const_typeless: term list -> term -> bool
   val sym_trm : term -> term (* unused code, kept as hints to design ideas *)
 
-(*isac_test*)
+  val string_of_detail: Proof.context -> term -> string
+
+\<^isac_test>\<open>
   val mk_negative: typ -> term -> term
-  val free2var: term -> term
+  val mk_Var: term -> term
   val scala_of_term: term -> string
 
-(*val atom_typ: typ -> unit RENAME*)
-  val atomtyp: typ -> unit
-  val atomty: term -> unit
-  val atomw: term -> unit
-  val atomt: term -> unit
-  val atomwy: term -> unit
+  val atom_typ: Proof.context -> typ -> unit
+  val atom_write: Proof.context -> term -> unit
+  val atom_trace: Proof.context -> term -> unit
 
-\<^isac_test>\<open>
+  val atom_write_detail: Proof.context -> term -> unit
+  val atom_trace_detail: Proof.context -> term -> unit
 \<close>
 end
 
@@ -151,7 +150,20 @@
     handle Pattern.MATCH => false
 
 (** transform  typ / term to a String to be parsed by Scala after transport via libisabelle **)
-(*isac_test*)
+fun string_of_detail ctxt t =
+  let
+    fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
+      | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
+      | ato (Var ((a, i), T)) n =
+        "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
+      | ato (Bound i) n = "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
+      | ato (Abs(a, T, body))  n = 
+        "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ",.." ^ ato body (n + 1)
+      | ato (f $ t) n = ato f n ^ ato t (n + 1)
+  in "\n*** " ^ ato t 0 ^ "\n***" end;
+
+
+\<^isac_test>\<open>
 fun scala_of_typ (Type (s, typs)) =
     enclose "Type(" ")" (quote s ^ ", " ^
       (typs |> map scala_of_typ |> commas |> enclose "List(" ")"))
@@ -181,7 +193,7 @@
 
 (* see structure's bare bones.
    for Isabelle standard output compare 2017 "structure ML_PP" *)
-fun atomtyp t =
+fun atom_typ ctxt t =
   let
     fun ato n (Type (s, [])) = "\n*** " ^ indent n ^ "Type (" ^ s ^",[])"
       | ato n (Type (s, Ts)) = "\n*** " ^ indent n ^ "Type (" ^ s ^ ",[" ^ atol (n + 1) Ts
@@ -201,31 +213,12 @@
 	  | ato (Abs (a, _, body)) n = "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
 	  | ato (f $ t) n = (ato f n ^ ato t (n + 1))
 in
-  fun atomw t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***");
-  fun atomt t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***");
+  fun atom_write _ t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***");
+  fun atom_trace _ t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***");
 end;
 
-\<^isac_test>\<open>
-\<close>
-
-fun term_detail2str t =
-  let
-    val ctxt = "Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global
-    fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
-      | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
-      | ato (Var ((a, i), T)) n =
-        "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ_in_ctxt ctxt T ^ ")"
-      | ato (Bound i) n = "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
-      | ato (Abs(a, T, body))  n = 
-        "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ",.." ^ ato body (n + 1)
-      | ato (f $ t) n = ato f n ^ ato t (n + 1)
-  in "\n*** " ^ ato t 0 ^ "\n***" end;
-
-(*isac_test*)
-fun atomwy t = (writeln o term_detail2str) t;
-fun atomty t = (tracing o term_detail2str) t;
-
-\<^isac_test>\<open>
+fun atom_write_detail ctxt t = (writeln o (string_of_detail ctxt)) t;
+fun atom_trace_detail ctxt t = (tracing o (string_of_detail ctxt)) t;
 \<close>
 
 (* contains the term a VAR(("*",_),_) ? *)
@@ -365,16 +358,15 @@
   | var2free (Abs(s, T, t)) = Abs(s, T, var2free t)
   | var2free (t1 $ t2) = (var2free t1) $ (var2free t2);
   
-(*isac_test*)
+
+\<^isac_test>\<open> (*TODO: check with new numerals --vv*)
 (* Logic.varify does NOT take care of 'Free ("1", _)'*)
-fun free2var (t as Const _) = t
-  | free2var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T)
-  | free2var (t as Var _) = t
-  | free2var (t as Bound _) = t 
-  | free2var (Abs (s, T, t)) = Abs (s, T, free2var t)
-  | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
-
-\<^isac_test>\<open>
+fun mk_Var (t as Const _) = t
+  | mk_Var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T)
+  | mk_Var (t as Var _) = t
+  | mk_Var (t as Bound _) = t 
+  | mk_Var (Abs (s, T, t)) = Abs (s, T, mk_Var t)
+  | mk_Var (t1 $ t2) = (mk_Var t1) $ (mk_Var t2);
 \<close>
 
 fun mk_listT T = Type (\<^type_name>\<open>list\<close>, [T]);