1.1 --- a/src/Tools/isac/MathEngBasic/method.sml	Tue May 12 16:22:00 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/method.sml	Tue May 12 17:42:29 2020 +0200
     1.3 @@ -11,7 +11,9 @@
     1.4    type id = Meth_Def.id
     1.5    val id_empty: id
     1.6    val id_to_string: id -> string
     1.7 -(*val metID2str: id -> string*)
     1.8 +
     1.9 +  val from_store: id -> T
    1.10 +  val from_store': theory -> id -> T
    1.11  
    1.12  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.13    (*NONE*)
    1.14 @@ -32,4 +34,8 @@
    1.15  val id_empty = Meth_Def.id_empty;
    1.16  val id_to_string = Meth_Def.id_to_string;
    1.17  
    1.18 +(* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
    1.19 +fun from_store metID = Store.get (get_mets ()) metID metID;
    1.20 +fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;
    1.21 +
    1.22  (**)end(**)