1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Aug 14 18:13:37 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sat Aug 14 18:49:36 2021 +0200
1.3 @@ -123,15 +123,16 @@
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_in_thy thy f ^ "\" @ \"[" ^
1.8 + val _ = tracing ("t= f @ ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^
1.9 commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");
1.10 - val _ = tracing ("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
1.11 + val _ = tracing ("u= g @ us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
1.12 commas (map (UnparseC.term_in_thy thy) us) ^ "]\"");
1.13 - val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
1.14 + val _ = tracing ("size_of_term (t, u) = (" ^ string_of_int (size_of_term' t) ^ ", " ^
1.15 string_of_int (size_of_term' u) ^ ")");
1.16 - val _ = tracing ("hd_ord(f,g) = " ^ ((pr_ord o hd_ord) (f,g)));
1.17 - val _ = tracing ("terms_ord (ts,us) = " ^(pr_ord o terms_ord str false) (ts,us));
1.18 - val _=tracing("-------");
1.19 + val _ = tracing ("hd_ord (f, g) = " ^ ((pr_ord o hd_ord) (f, g)) );
1.20 + (** )val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}( **)
1.21 + val _ = tracing ("terms_ord (ts, us) = " ^(pr_ord o terms_ord str false) (ts,us));
1.22 + val _= tracing ("-------");
1.23 in () end
1.24 else ();
1.25 case int_ord (size_of_term' t, size_of_term' u) of