equal
deleted
inserted
replaced
39 |
39 |
40 |
40 |
41 (* errors *) |
41 (* errors *) |
42 |
42 |
43 fun err_method name kind = |
43 fun err_method name kind = |
44 error ("Error while invoking " ^ name ^ " method of " ^ quote kind ^ " data"); |
44 error ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method"); |
45 |
45 |
46 fun err_dup_init kind = |
46 fun err_dup_init kind = |
47 error ("Duplicate initialization of " ^ quote kind ^ " data"); |
47 error ("Duplicate initialization of " ^ quote kind ^ " data"); |
48 |
48 |
49 fun err_uninit kind = |
49 fun err_uninit kind = |