1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Thu Aug 04 16:48:37 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Fri Aug 05 08:45:37 2022 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4  val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty 
     1.5  			 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
     1.6  			  (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
     1.7 -			  Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_"),
     1.8 +			  Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
     1.9  			  Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
    1.10  			  ];
    1.11  val SOME (t',_) = rewrite_set_ ctxt false testrls t;
    1.12 @@ -382,7 +382,7 @@
    1.13  #####  try calc: op <'
    1.14  ###  asms accepted: ["1 < 2 + - 1"]   stored: ["1 < 2 + - 1"]
    1.15  
    1.16 -... i.e Eval ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
    1.17 +... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
    1.18  (*--------------------------------------------------------------------------------------------//*)
    1.19  
    1.20