(* Title:  Interpret/lucas-interpreter.sml

    Author: Walther Neuper 2019

    (c) due to copyright terms

 *)

 signature METHOD =

 sig

   type T = Meth_Def.T

   val empty: T

   type id = Meth_Def.id

   val id_empty: id

   val id_to_string: id -> string

   val from_store: id -> T

   val from_store': theory -> id -> T

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (*NONE*)

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   (*NONE*)

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 (**)

 structure Method(**): METHOD(**) =

 struct

 (**)

 type T = Meth_Def.T;

 val empty = Meth_Def.empty;

 type id = Meth_Def.id;

 val id_empty = Meth_Def.id_empty;

 val id_to_string = Meth_Def.id_to_string;

 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)

 fun from_store metID = Store.get (get_mets ()) metID metID;

 fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;

 (**)end(**)