diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/MathEngBasic/rewrite.sml
--- a/test/Tools/isac/MathEngBasic/rewrite.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -88,7 +88,7 @@
 val thm =  @{thm add.commute};
 val tm = @{term "x + y*z::real"};
 
-val SOME (r,_) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
+val SOME (r,_) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
 (*is displayed on _TOP_ of <response> buffer...*)
 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
 if r = @{term "y*z + x::real"}
@@ -97,7 +97,7 @@
 "----- rewriting a subterm";
 val tm = @{term "w*(x + y*z)::real"};
 
-val SOME (r, _) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
+val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
 
 "----- ordered rewriting";
 fun tord (_:subst) pp = LibraryC.termless pp;
@@ -150,7 +150,7 @@
 val thm =  @{thm nonzero_divide_mult_cancel_right};
 val tm = @{term "x / (2 * x)::real"};
 
-val SOME (rew, asm) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
+val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
 
 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
 else error "rewrite.sml diff.result in cond.rew.";
@@ -168,12 +168,12 @@
 val tm = @{term "x / (2 * x)::real"};
 val erls = eval_rls;
 
-(**)val SOME (rew, asm) = rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm;
+(**)val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
   dest_Trueprop
   ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
-  (thy, dummy_ord, erls, false, thm, tm);
+  (thy, Rewrite_Ord.function_empty, erls, false, thm, tm);
 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
   (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);
 
@@ -210,11 +210,11 @@
 "----------- step through 'and rew_sub': ----------------";
 (*and make asms without Trueprop, beginning with the result:*)
 val tm = @{term "x / (2 * x)::real"};
-val (t', asm, _, _) = rew_sub ctxt 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
+val (t', asm, _, _) = rew_sub ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true [] (Thm.prop_of thm) tm;
 (*show_types := false;*)
 "----- evaluate arguments";
 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
-    (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
+    (thy, 0, [], Rewrite_Ord.function_empty, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
 "----- step 1: LHS, RHS of rule";
      val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
                        o Logic.strip_imp_concl) r;
@@ -245,7 +245,7 @@
 "----------- step through 'fun rewrite_terms_'  ------------------------------------------------";
 "----- step 0: args for rewrite_terms_, local fun";
 val (thy, ord, erls, equs, t) =
-    (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
+    (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.str2term "x = 0"],
      TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
 "----- step 1: args for rew_";
 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
@@ -254,21 +254,21 @@
 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
 
 
-val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
+val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
 writeln "---------- rewrite_terms_  1---------------------------";
 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
 else error "rewrite.sml rewrite_terms_ [x = 0]";
 
 val equs = [TermC.str2term "M_b 0 = 0"];
 val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
-val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
+val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
 writeln "---------- rewrite_terms_  2---------------------------";
 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
 
 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
 val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
-val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
+val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
 writeln "---------- rewrite_terms_  3---------------------------";
 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
@@ -658,7 +658,7 @@
 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
-  (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
+  (@{theory}, Rewrite_Ord.function_empty, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
   (thy, 1, [], rew_ord, erls, bool, thm, term);
 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =