test/Tools/isac/Knowledge/rational-2.sml
changeset 60509 2e0b7ca391dc
parent 60504 8cc1415b3530
child 60543 9555ee96e046
     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