diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -439,7 +439,7 @@
 val rearrange_assoc =
   Rule_Def.Repeat{
     id = "rearrange_assoc", preconds = [], 
-    rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), 
+    rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), 
     erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm_sym>\<open>add.assoc\<close>,
@@ -461,7 +461,7 @@
 
 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
 val norm_equation =
-  Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+  Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
     erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>rnorm_equation_add\<close>],
@@ -525,7 +525,7 @@
 ML \<open>
 (*isolate the root in a root-equation*)
 val isolate_root =
-  Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), 
+  Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), 
     erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
     rules = [
        \<^rule_thm>\<open>rroot_to_lhs\<close>,
@@ -539,7 +539,7 @@
 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
 val isolate_bdv =
   Rule_Def.Repeat{
-    id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
+    id = "isolate_bdv", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
   	erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
   	rules = [
       \<^rule_thm>\<open>risolate_bdv_add\<close>,
@@ -777,7 +777,7 @@
   in
     [e_e])"
 method met_test_solvelin : "Test/solve_linear" =
-  \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
+  \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
     prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
     nrls = Test_simplify}\<close>
   Program: solve_linear.simps
@@ -808,7 +808,7 @@
 
 method met_test_sqrt : "Test/sqrt-equ-test" =
   (*root-equation, version for tests before 8.01.01*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
         [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
     prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty 
@@ -834,7 +834,7 @@
 
 method met_test_squ_sub : "Test/squ-equ-test-subpbl1" =
   (*tests subproblem fixed linear*)
-  \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
+  \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
      prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
        [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],
      calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close>
@@ -864,7 +864,7 @@
 
 method met_test_eq1 : "Test/square_equation1" =
   (*root-equation1:*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty 
       [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
     prls=Rule_Set.empty, calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
@@ -894,7 +894,7 @@
 
 method met_test_squ2 : "Test/square_equation2" =
   (*root-equation2*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty 
       [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
     prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
@@ -924,7 +924,7 @@
 
 method met_test_squeq : "Test/square_equation" =
   (*root-equation*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
     srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty 
       [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
     prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
@@ -947,7 +947,7 @@
 
 method met_test_eq_plain : "Test/solve_plain_square" =
   (*solve_plain_square*)
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
     prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
     asm_rls=[],asm_thm=[]*)}\<close>
   Program: solve_plain_square.simps
@@ -974,7 +974,7 @@
         [''no_met'']) [BOOL e_e, REAL v_v])"
 
 method met_test_norm_univ : "Test/norm_univar_equation" =
-  \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
+  \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
     errpats = [], nrls = Rule_Set.empty}\<close>
   Program: norm_univariate_equ.simps
   Given: "equality e_e" "solveFor v_v"
@@ -992,7 +992,7 @@
     (Try (Calculate ''TIMES''))) t_t)"
 
 method met_test_intsimp : "Test/intsimp" =
-  \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,  prls = Rule_Set.empty, calc = [],
+  \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,  prls = Rule_Set.empty, calc = [],
     crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
   Program: test_simplify.simps
   Given: "intTestGiven t_t"