1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Sat May 09 13:15:25 2020 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Sat May 09 15:31:15 2020 +0200
     1.3 @@ -1255,20 +1255,20 @@
     1.4     val iii = appl_adds dI oris ppc pbt (selct::ss); 
     1.5     tracing(I_Model.to_string thy iii);
     1.6  
     1.7 - val itm = appl_add' dI oris ppc pbt selct;
     1.8 + val itm = add_single' dI oris ppc pbt selct;
     1.9   val ppc = insert_ppc' itm ppc;
    1.10  
    1.11   val _::selct::ss = (selct::ss);
    1.12 - val itm = appl_add' dI oris ppc pbt selct;
    1.13 + val itm = add_single' dI oris ppc pbt selct;
    1.14   val ppc = insert_ppc' itm ppc;
    1.15  
    1.16   val _::selct::ss = (selct::ss);
    1.17 - val itm = appl_add' dI oris ppc pbt selct;
    1.18 + val itm = add_single' dI oris ppc pbt selct;
    1.19   val ppc = insert_ppc' itm ppc;
    1.20   tracing(I_Model.to_string thy ppc);
    1.21  
    1.22   val _::selct::ss = (selct::ss);
    1.23 - val itm = appl_add' dI oris ppc pbt selct;
    1.24 + val itm = add_single' dI oris ppc pbt selct;
    1.25   val ppc = insert_ppc' itm ppc;
    1.26     *)
    1.27  "--------- fun concat_deriv --------------------------------------";