1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Nov 19 07:51:41 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Nov 20 10:49:54 2023 +0100
     1.3 @@ -104,6 +104,7 @@
     1.4    val string_of_detail: Proof.context -> term -> string
     1.5  (*from isac_test for Minisubpbl*)
     1.6    val atom_typ: Proof.context -> typ -> unit
     1.7 +  val atom_trace_detail: Proof.context -> term -> unit
     1.8  
     1.9  \<^isac_test>\<open>
    1.10    val mk_negative: typ -> term -> term
    1.11 @@ -114,7 +115,7 @@
    1.12    val atom_trace: Proof.context -> term -> unit
    1.13  
    1.14    val atom_write_detail: Proof.context -> term -> unit
    1.15 -  val atom_trace_detail: Proof.context -> term -> unit
    1.16 +(*val atom_trace_detail: Proof.context -> term -> unit*)
    1.17  \<close>
    1.18  end
    1.19  
    1.20 @@ -221,8 +222,8 @@
    1.21  end;
    1.22  
    1.23  fun atom_write_detail ctxt t = (writeln o (string_of_detail ctxt)) t;
    1.24 +\<close>
    1.25  fun atom_trace_detail ctxt t = (tracing o (string_of_detail ctxt)) t;
    1.26 -\<close>
    1.27  
    1.28  (* contains the term a VAR(("*",_),_) ? *)
    1.29  fun contains_Var (Abs(_,_,body)) = contains_Var body