1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Apr 13 13:13:07 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Apr 13 13:27:55 2020 +0200
     1.3 @@ -126,10 +126,10 @@
     1.4       then 
     1.5         let
     1.6           val (f, ts) = strip_comb t and (g, us) = strip_comb u;
     1.7 -         val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_thy thy f ^ "\" @ \"[" ^
     1.8 -           commas (map (UnparseC.term_thy thy) ts) ^ "]\"");
     1.9 -         val _ = tracing ("u= g@us= \"" ^ UnparseC.term_thy thy g ^ "\" @ \"[" ^
    1.10 -           commas (map (UnparseC.term_thy thy) us) ^ "]\"");
    1.11 +         val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^
    1.12 +           commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");
    1.13 +         val _ = tracing ("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
    1.14 +           commas (map (UnparseC.term_in_thy thy) us) ^ "]\"");
    1.15           val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
    1.16             string_of_int (size_of_term' u) ^ ")");
    1.17           val _ = tracing ("hd_ord(f,g)      = " ^ ((pr_ord o hd_ord) (f,g)));