test/Tools/isac/Knowledge/algein.sml
changeset 60565 f92963a33fe3
parent 60549 c0a775618258
child 60567 bb3140a02f3d
     1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4  val rew_ord = Rewrite_Ord.function_empty;
     1.5  val erls = Rule_Set.Empty;
     1.6  val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
     1.7 -val t = TermC.str2term "0 = (0::real)";
     1.8 +val t = TermC.parse_test @{context} "0 = (0::real)";
     1.9  val SOME (t',_) = rewrite_ ctxt rew_ord erls false thm t;
    1.10  UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
    1.11