1.1 --- a/TODO.md	Sat Aug 14 18:13:37 2021 +0200
     1.2 +++ b/TODO.md	Sat Aug 14 18:49:36 2021 +0200
     1.3 @@ -57,7 +57,10 @@
     1.4      https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210
     1.5  
     1.6  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
     1.7 -      ???
     1.8 +    takes only static arguments ----------------^^^^^^^^^^^^^^, not value of "hd_ord (f, g)"
     1.9 +    ? are there better approximations to old output of (*1*) than with (*2*)
    1.10 +    (*1*)val _ = tracing ("hd_ord (f, g)      = " ^ ((pr_ord o hd_ord) (f, g)) );
    1.11 +    (*2*)val _ = @{print tracing}{a = "hd_ord (f, g)      = ", z = hd_ord (f, g)}(**)
    1.12  
    1.13  * WN: reduce the number of TermC.parse*;
    1.14    + 0d22a6bf1fc6 was too much for 1 changeset

     2.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Sat Aug 14 18:13:37 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sat Aug 14 18:49:36 2021 +0200
     2.3 @@ -123,15 +123,16 @@
     2.4       then 
     2.5         let
     2.6           val (f, ts) = strip_comb t and (g, us) = strip_comb u;
     2.7 -         val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^
     2.8 +         val _ = tracing ("t= f @ ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^
     2.9             commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");
    2.10 -         val _ = tracing ("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
    2.11 +         val _ = tracing ("u= g @ us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
    2.12             commas (map (UnparseC.term_in_thy thy) us) ^ "]\"");
    2.13 -         val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
    2.14 +         val _ = tracing ("size_of_term (t, u) = (" ^ string_of_int (size_of_term' t) ^ ", " ^
    2.15             string_of_int (size_of_term' u) ^ ")");
    2.16 -         val _ = tracing ("hd_ord(f,g)      = " ^ ((pr_ord o hd_ord) (f,g)));
    2.17 -         val _ = tracing ("terms_ord (ts,us) = " ^(pr_ord o terms_ord str false) (ts,us));
    2.18 -         val _=tracing("-------");
    2.19 +         val _ = tracing ("hd_ord (f, g)      = " ^ ((pr_ord o hd_ord) (f, g)) );
    2.20 +    (** )val _ = @{print tracing}{a = "hd_ord (f, g)      = ", z = hd_ord (f, g)}( **)
    2.21 +         val _ = tracing ("terms_ord (ts, us) = " ^(pr_ord o terms_ord str false) (ts,us));
    2.22 +         val _= tracing ("-------");
    2.23         in () end
    2.24       else ();
    2.25      case int_ord (size_of_term' t, size_of_term' u) of