diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -158,12 +158,12 @@
 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
 val norm_Rational_rls_noadd_fractions = 
   Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [], 
-    rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+    rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
     erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
   	  Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
   		(Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], 
-  		   rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+  		   rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
   		   erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
   				 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
   			 srls = Rule_Set.Empty, calc = [], errpatts = [],
@@ -187,7 +187,7 @@
 (*.for simplify_Integral adapted from 'norm_Rational'.*)
 val norm_Rational_noadd_fractions = 
   Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [], 
-    rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
+    rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
     erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [Rule.Rls_ discard_minus,
   		Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c    *)
@@ -214,7 +214,7 @@
 		];
 val simplify_Integral = 
   Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list, 
-    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
+    rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
     erls = Atools_erls, srls = Rule_Set.Empty,
     calc = [],  errpatts = [],
     rules = [