| changeset 6262 | 0ebfcf181d84 |
| parent 6240 | 3231375b701f |
| child 6275 | c8b30f86aadf |
--- a/src/Pure/Thy/session.ML Mon Feb 08 17:31:50 1999 +0100 +++ b/src/Pure/Thy/session.ML Mon Feb 08 17:32:06 1999 +0100 @@ -42,7 +42,7 @@ fun init reset parent name = if not (parent mem_string (! session)) orelse not (! session_finished) then - error ("Unfinished parent session " ^ quote (str_of (! session)) ^ " for " ^ quote name) + error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) else (add_path reset name; session_finished := false);