1.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Fri Aug 05 11:38:10 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Fri Aug 05 11:41:06 2022 +0200
     1.3 @@ -48,18 +48,5 @@
     1.4  ML \<open>
     1.5  \<close> ML \<open>
     1.6  \<close> ML \<open>
     1.7 -fun from_store id = Store.get (get_pbls ()) id (rev id);
     1.8 -\<close> ML \<open>
     1.9 -from_store: Store.key -> Probl_Def.T
    1.10 -\<close> ML \<open>
    1.11 -fun from_store id =
    1.12 -  (Store.get (get_pbls ()) id (rev id))
    1.13 -    handle ERROR _ =>
    1.14 -      raise error ("*** ERROR Problem.from_store " ^ strs2str id ^ " not found");
    1.15 -\<close> ML \<open>
    1.16 -\<close> ML \<open>
    1.17 -\<close> ML \<open>
    1.18 -\<close> ML \<open>
    1.19 -\<close> ML \<open>
    1.20  \<close>
    1.21  end