src/Tools/isac/Knowledge/LinEq.thy
changeset 59857 cbb3fae0381d
parent 59852 ea7e6679080e
child 59871 82428ca0d23e
     1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Apr 08 15:50:03 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Apr 08 16:56:47 2020 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
     1.5  val LinEq_simplify = prep_rls'(
     1.6  Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
     1.7 -     rew_ord = ("e_rew_ord", Rule.e_rew_ord),
     1.8 +     rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
     1.9       erls = LinEq_erls,
    1.10       srls = Rule_Set.Empty,
    1.11       calc = [], errpatts = [],