1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Wed Aug 03 18:17:27 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Thu Aug 04 12:48:37 2022 +0200
1.3 @@ -854,7 +854,7 @@
1.4 "HOL.True";
1.5
1.6 val t = TermC.str2term "(6*x) \<up> 2";
1.7 -val SOME (t',_) = rewrite_ ctxt dummy_ord powers_erls false @{thm realpow_def_atom} t;
1.8 +val SOME (t',_) = rewrite_ ctxt Rewrite_Ord.function_empty powers_erls false @{thm realpow_def_atom} t;
1.9 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then ()
1.10 else error "rational.sml powers_erls (6*x) \<up> 2";
1.11