diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/LinEq.thy --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Aug 03 18:17:27 2022 +0200 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Aug 04 12:48:37 2022 +0200 @@ -88,7 +88,7 @@ (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*) val LinEq_simplify = prep_rls'( Rule_Def.Repeat {id = "LinEq_simplify", preconds = [], - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), + rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), erls = LinEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],