1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Tue Jul 13 15:28:43 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Jul 15 14:10:18 2021 +0200
     1.3 @@ -157,8 +157,8 @@
     1.4      (term_ord' pr thy (Library.swap tu) = LESS);*)
     1.5  
     1.6  (*for the rls's*)
     1.7 -fun ord_simplify_System (pr:bool) thy _(*subst*) tu = 
     1.8 -    (term_ord' pr thy tu = LESS);
     1.9 +fun ord_simplify_System (pr:bool) thy _(*subst*) (ts, us) = 
    1.10 +    (term_ord' pr thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS);
    1.11  (**)
    1.12  end;
    1.13  (**)