1.1 --- a/test/Tools/isac/Interpret/inform.sml	Tue Nov 22 10:42:21 2016 +0100
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Thu Nov 24 14:33:42 2016 +0100
     1.3 @@ -38,6 +38,7 @@
     1.4  "--------- build fun get_fillpats --------------------------------";
     1.5  "--------- embed fun find_fillpatterns ---------------------------";
     1.6  "--------- build fun is_exactly_equal, inputFillFormula ----------";
     1.7 +"--------- fun appl_adds -----------------------------------------";
     1.8  "-----------------------------------------------------------------";
     1.9  "-----------------------------------------------------------------";
    1.10  "-----------------------------------------------------------------";
    1.11 @@ -1292,3 +1293,32 @@
    1.12      | _ => error "inputFillFormula changed 112"
    1.13    else error "inputFillFormula changed 113";
    1.14  
    1.15 +"--------- fun appl_adds -----------------------------------------";
    1.16 +"--------- fun appl_adds -----------------------------------------";
    1.17 +"--------- fun appl_adds -----------------------------------------";
    1.18 +(* val (dI, oris, ppc, pbt, selct::ss) = 
    1.19 +       (dI, pors, probl, ppc, map itms2fstr probl);
    1.20 +   ...vvv
    1.21 +   *)
    1.22 +(* val (dI, oris, ppc, pbt, (selct::ss))=
    1.23 +       (#1 (some_spec ospec spec), oris, []:itm list,
    1.24 +	((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
    1.25 +   val iii = appl_adds dI oris ppc pbt (selct::ss); 
    1.26 +   tracing(itms2str_ thy iii);
    1.27 +
    1.28 + val itm = appl_add' dI oris ppc pbt selct;
    1.29 + val ppc = insert_ppc' itm ppc;
    1.30 +
    1.31 + val _::selct::ss = (selct::ss);
    1.32 + val itm = appl_add' dI oris ppc pbt selct;
    1.33 + val ppc = insert_ppc' itm ppc;
    1.34 +
    1.35 + val _::selct::ss = (selct::ss);
    1.36 + val itm = appl_add' dI oris ppc pbt selct;
    1.37 + val ppc = insert_ppc' itm ppc;
    1.38 + tracing(itms2str_ thy ppc);
    1.39 +
    1.40 + val _::selct::ss = (selct::ss);
    1.41 + val itm = appl_add' dI oris ppc pbt selct;
    1.42 + val ppc = insert_ppc' itm ppc;
    1.43 +   *)