1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -909,7 +909,7 @@
     1.4  val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2");
     1.5  
     1.6  val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
     1.7 -  rew_sub ctxt 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
     1.8 +  rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
     1.9  if rewritten then NONE else SOME "e_errpatID";
    1.10  
    1.11  val norm_res = case rewrite_set_ ctxt false rls res' of
    1.12 @@ -957,7 +957,7 @@
    1.13  val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)");
    1.14  
    1.15  val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
    1.16 -  rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.17 +  rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
    1.18  if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then ()
    1.19  else error "build fun check_for' ?bdv changed 2";
    1.20  
    1.21 @@ -1119,7 +1119,7 @@
    1.22    val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
    1.23    (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
    1.24  val (form', _, _, rewritten) =
    1.25 -      rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    1.26 +      rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    1.27  
    1.28  if UnparseC.term form' = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" then ()
    1.29  else error "find_fill_patterns changed 3";