diff -r b24adc7c9875 -r 05e5a8498634 test/Tools/isac/Interpret/error-pattern.sml
--- a/test/Tools/isac/Interpret/error-pattern.sml	Sat May 09 13:15:25 2020 +0200
+++ b/test/Tools/isac/Interpret/error-pattern.sml	Sat May 09 15:31:15 2020 +0200
@@ -1255,20 +1255,20 @@
    val iii = appl_adds dI oris ppc pbt (selct::ss); 
    tracing(I_Model.to_string thy iii);
 
- val itm = appl_add' dI oris ppc pbt selct;
+ val itm = add_single' dI oris ppc pbt selct;
  val ppc = insert_ppc' itm ppc;
 
  val _::selct::ss = (selct::ss);
- val itm = appl_add' dI oris ppc pbt selct;
+ val itm = add_single' dI oris ppc pbt selct;
  val ppc = insert_ppc' itm ppc;
 
  val _::selct::ss = (selct::ss);
- val itm = appl_add' dI oris ppc pbt selct;
+ val itm = add_single' dI oris ppc pbt selct;
  val ppc = insert_ppc' itm ppc;
  tracing(I_Model.to_string thy ppc);
 
  val _::selct::ss = (selct::ss);
- val itm = appl_add' dI oris ppc pbt selct;
+ val itm = add_single' dI oris ppc pbt selct;
  val ppc = insert_ppc' itm ppc;
    *)
 "--------- fun concat_deriv --------------------------------------";