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