1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Mon Apr 19 11:45:43 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Mon Apr 19 15:02:00 2021 +0200
     1.3 @@ -29,8 +29,8 @@
     1.4  \ (let t_t = (l_l = 1)\
     1.5  \ in t_t)"
     1.6  ;
     1.7 -val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
     1.8 -atomty sc;
     1.9 +val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
    1.10 +TermC.atomty sc;
    1.11  atomt sc;
    1.12  
    1.13  "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
    1.14 @@ -104,7 +104,7 @@
    1.15  val rew_ord = dummy_ord;
    1.16  val erls = Rule_Set.Empty;
    1.17  val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
    1.18 -val t = str2term "0 = (0::real)";
    1.19 +val t = TermC.str2term "0 = (0::real)";
    1.20  val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
    1.21  UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
    1.22  
    1.23 @@ -112,7 +112,7 @@
    1.24  val subte = Subst.input_to_terms sube;
    1.25  UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)
    1.26  val subst = Subst.T_from_string_eqs thy sube;
    1.27 -foldl and_ (true, map contains_Var subte);
    1.28 +foldl and_ (true, map TermC.contains_Var subte);
    1.29  
    1.30  val t'' = subst_atomic subst t';
    1.31  UnparseC.term t'' = "0 = 3 * 0"; (* = true*)