1.1 --- a/TODO.md	Fri Aug 05 08:45:37 2022 +0200
     1.2 +++ b/TODO.md	Fri Aug 05 11:38:10 2022 +0200
     1.3 @@ -67,8 +67,6 @@
     1.4  
     1.5  ***** priority of WN items is top down, most urgent/simple on top
     1.6  
     1.7 -* WN: MethodC.from_store throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument
     1.8 -
     1.9  * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
    1.10      - Prconditions.eval
    1.11      - Solve_Step.check ..Rewrite_Inst, Substitute, ..

     2.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Fri Aug 05 08:45:37 2022 +0200
     2.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Fri Aug 05 11:38:10 2022 +0200
     2.3 @@ -48,5 +48,18 @@
     2.4  ML \<open>
     2.5  \<close> ML \<open>
     2.6  \<close> ML \<open>
     2.7 +fun from_store id = Store.get (get_pbls ()) id (rev id);
     2.8 +\<close> ML \<open>
     2.9 +from_store: Store.key -> Probl_Def.T
    2.10 +\<close> ML \<open>
    2.11 +fun from_store id =
    2.12 +  (Store.get (get_pbls ()) id (rev id))
    2.13 +    handle ERROR _ =>
    2.14 +      raise error ("*** ERROR Problem.from_store " ^ strs2str id ^ " not found");
    2.15 +\<close> ML \<open>
    2.16 +\<close> ML \<open>
    2.17 +\<close> ML \<open>
    2.18 +\<close> ML \<open>
    2.19 +\<close> ML \<open>
    2.20  \<close>
    2.21  end

     3.1 --- a/src/Tools/isac/MathEngBasic/method.sml	Fri Aug 05 08:45:37 2022 +0200
     3.2 +++ b/src/Tools/isac/MathEngBasic/method.sml	Fri Aug 05 11:38:10 2022 +0200
     3.3 @@ -143,7 +143,14 @@
     3.4  (** get MethodC from Store **)
     3.5  
     3.6  (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
     3.7 -fun from_store metID = Store.get (get_mets ()) metID metID;
     3.8 -fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;
     3.9 +fun from_store id =
    3.10 +  (Store.get (get_mets ()) id id)
    3.11 +    handle ERROR _ =>
    3.12 +      raise error ("*** ERROR MethodC.from_store " ^ strs2str id ^ " not found");
    3.13 +
    3.14 +fun from_store' thy id =
    3.15 +  (Store.get (KEStore_Elems.get_mets thy) id id)
    3.16 +    handle ERROR _ =>
    3.17 +      raise error ("*** ERROR MethodC.from_store thy " ^ strs2str id ^ " not found");
    3.18  
    3.19  (**)end(**)

     4.1 --- a/src/Tools/isac/MathEngBasic/problem.sml	Fri Aug 05 08:45:37 2022 +0200
     4.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml	Fri Aug 05 11:38:10 2022 +0200
     4.3 @@ -278,6 +278,9 @@
     4.4  
     4.5  (** get Problem from Store **)
     4.6  
     4.7 -fun from_store id = Store.get (get_pbls ()) id (rev id);
     4.8 +fun from_store id =
     4.9 +  (Store.get (get_pbls ()) id (rev id))
    4.10 +    handle ERROR _ =>
    4.11 +      raise error ("*** ERROR Problem.from_store " ^ strs2str id ^ " not found");
    4.12  
    4.13  (**)end(**)