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