equal
deleted
inserted
replaced
46 ML_file calculation.sml |
46 ML_file calculation.sml |
47 |
47 |
48 ML \<open> |
48 ML \<open> |
49 \<close> ML \<open> |
49 \<close> ML \<open> |
50 \<close> ML \<open> |
50 \<close> ML \<open> |
|
51 fun from_store id = Store.get (get_pbls ()) id (rev id); |
|
52 \<close> ML \<open> |
|
53 from_store: Store.key -> Probl_Def.T |
|
54 \<close> ML \<open> |
|
55 fun from_store id = |
|
56 (Store.get (get_pbls ()) id (rev id)) |
|
57 handle ERROR _ => |
|
58 raise error ("*** ERROR Problem.from_store " ^ strs2str id ^ " not found"); |
|
59 \<close> ML \<open> |
|
60 \<close> ML \<open> |
|
61 \<close> ML \<open> |
|
62 \<close> ML \<open> |
|
63 \<close> ML \<open> |
51 \<close> |
64 \<close> |
52 end |
65 end |