1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Fri Apr 10 16:16:09 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Fri Apr 10 18:32:36 2020 +0200
     1.3 @@ -72,9 +72,9 @@
     1.4  			  (p as (Const ("EqSystem.occur'_exactly'_in",_) 
     1.5  				       $ vs $ all $ t)) _ =
     1.6      if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t
     1.7 -    then SOME ((UnparseC.term2str p) ^ " = True",
     1.8 +    then SOME ((UnparseC.term p) ^ " = True",
     1.9  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.10 -    else SOME ((UnparseC.term2str p) ^ " = False",
    1.11 +    else SOME ((UnparseC.term p) ^ " = False",
    1.12  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.13    | eval_occur_exactly_in _ _ _ _ = NONE;
    1.14  \<close>
    1.15 @@ -126,10 +126,10 @@
    1.16       then 
    1.17         let
    1.18           val (f, ts) = strip_comb t and (g, us) = strip_comb u;
    1.19 -         val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_to_string''' thy f ^ "\" @ \"[" ^
    1.20 -           commas (map (UnparseC.term_to_string''' thy) ts) ^ "]\"");
    1.21 -         val _ = tracing ("u= g@us= \"" ^ UnparseC.term_to_string''' thy g ^ "\" @ \"[" ^
    1.22 -           commas (map (UnparseC.term_to_string''' thy) us) ^ "]\"");
    1.23 +         val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_thy thy f ^ "\" @ \"[" ^
    1.24 +           commas (map (UnparseC.term_thy thy) ts) ^ "]\"");
    1.25 +         val _ = tracing ("u= g@us= \"" ^ UnparseC.term_thy thy g ^ "\" @ \"[" ^
    1.26 +           commas (map (UnparseC.term_thy thy) us) ^ "]\"");
    1.27           val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
    1.28             string_of_int (size_of_term' u) ^ ")");
    1.29           val _ = tracing ("hd_ord(f,g)      = " ^ ((pr_ord o hd_ord) (f,g)));