1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Apr 08 15:50:03 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Apr 08 16:56:47 2020 +0200
     1.3 @@ -163,12 +163,12 @@
     1.4  (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
     1.5  val norm_Rational_rls_noadd_fractions = 
     1.6  Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [], 
     1.7 -     rew_ord = ("dummy_ord",Rule.dummy_ord), 
     1.8 +     rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
     1.9       erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.10       rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
    1.11  	      Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
    1.12  		  (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], 
    1.13 -		       rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.14 +		       rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.15  		       erls = (*FIXME.WN051028 Rule_Set.empty,*)
    1.16  		       Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
    1.17  				  [Rule.Num_Calc ("Poly.is'_polyexp", 
    1.18 @@ -207,7 +207,7 @@
    1.19  (*.for simplify_Integral adapted from 'norm_Rational'.*)
    1.20  val norm_Rational_noadd_fractions = 
    1.21     Rule_Set.Seqence {id = "norm_Rational_noadd_fractions", preconds = [], 
    1.22 -       rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.23 +       rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.24         erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.25         rules = [Rule.Rls_ discard_minus,
    1.26  		Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c    *)
    1.27 @@ -241,7 +241,7 @@
    1.28  		];
    1.29  val simplify_Integral = 
    1.30    Rule_Set.Seqence {id = "simplify_Integral", preconds = []:term list, 
    1.31 -       rew_ord = ("dummy_ord", Rule.dummy_ord),
    1.32 +       rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.33        erls = Atools_erls, srls = Rule_Set.Empty,
    1.34        calc = [],  errpatts = [],
    1.35        rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
    1.36 @@ -267,7 +267,7 @@
    1.37  THIS IS KEPT FOR COMPARISON ............................................   
    1.38  * val simplify_Integral = prep_rls'(
    1.39  *   Rule_Set.Seqence {id = "", preconds = []:term list, 
    1.40 -*        rew_ord = ("dummy_ord", Rule.dummy_ord),
    1.41 +*        rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.42  *       erls = Atools_erls, srls = Rule_Set.Empty,
    1.43  *       calc = [], (*asm_thm = [],*)
    1.44  *       rules = [Rule.Rls_ expand_poly,