1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Thu Apr 09 12:03:14 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Thu Apr 09 17:13:17 2020 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  moveActiveRoot 1;
     1.5  autoCalculate 1 CompleteCalc;
     1.6  val ((pt,p),_) = get_calc 1; show_pt pt;
     1.7 -if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
     1.8 +if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) = "L = 104" then()
     1.9  else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
    1.10  
    1.11  "----------- Widerspruch 3 = 777 ---------------------------------";
    1.12 @@ -106,17 +106,17 @@
    1.13  val thm = assoc_thm' thy ("sym_mult_zero_right","");
    1.14  val t = str2term "0 = (0::real)";
    1.15  val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
    1.16 -term2str t' = "0 = ?a1 * 0"; (* = true*)
    1.17 +UnparseC.term2str t' = "0 = ?a1 * 0"; (* = true*)
    1.18  
    1.19  (*testing code in ME/appl.sml*)
    1.20  val sube = ["?a1 = (3::real)"];
    1.21  val subte = sube2subte sube;
    1.22 -terms2str' subte = "[?a1 = 3]"; (* = true*)
    1.23 +UnparseC.terms2str' subte = "[?a1 = 3]"; (* = true*)
    1.24  val subst = sube2subst thy sube;
    1.25  foldl and_ (true, map contains_Var subte);
    1.26  
    1.27  val t'' = subst_atomic subst t';
    1.28 -term2str t'' = "0 = 3 * 0"; (* = true*)
    1.29 +UnparseC.term2str t'' = "0 = 3 * 0"; (* = true*)
    1.30  
    1.31  val thm = assoc_thm' thy ("sym","");
    1.32  (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!