equal
deleted
inserted
replaced
141 in end; |
141 in end; |
142 |
142 |
143 (** get MethodC from Store **) |
143 (** get MethodC from Store **) |
144 |
144 |
145 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *) |
145 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *) |
146 fun from_store metID = Store.get (get_mets ()) metID metID; |
146 fun from_store id = |
147 fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID; |
147 (Store.get (get_mets ()) id id) |
|
148 handle ERROR _ => |
|
149 raise error ("*** ERROR MethodC.from_store " ^ strs2str id ^ " not found"); |
|
150 |
|
151 fun from_store' thy id = |
|
152 (Store.get (KEStore_Elems.get_mets thy) id id) |
|
153 handle ERROR _ => |
|
154 raise error ("*** ERROR MethodC.from_store thy " ^ strs2str id ^ " not found"); |
148 |
155 |
149 (**)end(**) |
156 (**)end(**) |