| changeset 4074 | 3a2aa65288df |
| parent 3989 | 092ab30c1471 |
| child 4124 | 1af16493c57f |
--- a/src/Pure/data.ML Mon Nov 03 11:46:25 1997 +0100 +++ b/src/Pure/data.ML Mon Nov 03 11:46:42 1997 +0100 @@ -41,7 +41,7 @@ (* errors *) fun err_method name kind = - error ("Error while invoking " ^ name ^ " method of " ^ quote kind ^ " data"); + error ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method"); fun err_dup_init kind = error ("Duplicate initialization of " ^ quote kind ^ " data");