1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Tue May 12 16:22:00 2020 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Tue May 12 17:42:29 2020 +0200
     1.3 @@ -47,9 +47,9 @@
     1.4  "--------- appendFormula: on Res + equ_nrls ----------------------";
     1.5  "--------- appendFormula: on Res + equ_nrls ----------------------";
     1.6  "--------- appendFormula: on Res + equ_nrls ----------------------";
     1.7 - val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
     1.8 + val Prog sc = (#scr o Method.from_store) ["Test","squ-equ-test-subpbl1"];
     1.9   (writeln o UnparseC.term) sc;
    1.10 - val Prog sc = (#scr o get_met) ["Test","solve_linear"];
    1.11 + val Prog sc = (#scr o Method.from_store) ["Test","solve_linear"];
    1.12   (writeln o UnparseC.term) sc;
    1.13  
    1.14   reset_states ();
    1.15 @@ -984,7 +984,7 @@
    1.16  val (res, inf) =
    1.17    (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
    1.18     str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
    1.19 -val {errpats, nrls = rls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]
    1.20 +val {errpats, nrls = rls, scr = Prog prog, ...} = Method.from_store ["diff", "differentiate_on_R"]
    1.21  
    1.22  val env = [(str2term "v_v", str2term "x")];
    1.23  val errpats =
    1.24 @@ -1032,16 +1032,16 @@
    1.25          (*if*) f_pred = f_in; (*else*)
    1.26            val NONE = (*case*) In_Chead.cas_input f_in (*of*);
    1.27         (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
    1.28 -       (*old*)val {scr = prog, ...} = Specify.get_met metID
    1.29 +       (*old*)val {scr = prog, ...} = Method.from_store metID
    1.30         (*old*)val istate = get_istate_LI pt pos
    1.31         (*old*)val ctxt = get_ctxt pt pos
    1.32         ( *old*)
    1.33         val LI.Not_Derivable =
    1.34               (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
    1.35              		  val pp = Ctree.par_pblobj pt p
    1.36 -            		  val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
    1.37 +            		  val (errpats, nrls, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
    1.38                		    {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
    1.39 -              		  | _ => error "inform: uncovered case of get_met"
    1.40 +              		  | _ => error "inform: uncovered case of Method.from_store"
    1.41  ;
    1.42  (*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\",\"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)\",\"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\",\"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\",\"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1) * d_d ?bdv ?u\",\"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\",\"d_d ?bdv (E_ ^^^ ?u) = E_ ^^^ ?u * d_d ?x ?u\"]]"
    1.43  (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
    1.44 @@ -1084,9 +1084,9 @@
    1.45  "~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
    1.46      val f_curr = Ctree.get_curr_formula (pt, pos);
    1.47      val pp = Ctree.par_pblobj pt p
    1.48 -    val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
    1.49 +    val (errpats, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
    1.50        {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
    1.51 -    | _ => error "find_fill_patterns: uncovered case of get_met"
    1.52 +    | _ => error "find_fill_patterns: uncovered case of Method.from_store"
    1.53      val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
    1.54      val subst = Subst.for_bdv prog env
    1.55      val errpatthms = errpats
    1.56 @@ -1105,7 +1105,7 @@
    1.57          val thmDeriv = Thm.get_name_hint thm
    1.58          val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
    1.59          val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
    1.60 -        val Thy_Write.Hthm {fillpats, ...} = get_the theID
    1.61 +        val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store theID
    1.62          val some = map (Error_Pattern.fill_form subst (thm, form) errpatID) fillpats;
    1.63  
    1.64  case some |> filter is_some |> map the of
    1.65 @@ -1251,7 +1251,7 @@
    1.66     *)
    1.67  (* val (dI, oris, ppc, pbt, (selct::ss))=
    1.68         (#1 (some_spec ospec spec), oris, []:I_Model.T,
    1.69 -	((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
    1.70 +	((#ppc o Problem.from_store) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
    1.71     val iii = appl_adds dI oris ppc pbt (selct::ss); 
    1.72     tracing(I_Model.to_string thy iii);
    1.73