--- a/src/Pure/Thy/thy_info.ML Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Sep 21 19:04:20 2006 +0200
@@ -352,8 +352,8 @@
val path = Path.expand (Path.unpack str);
val name = Path.pack (Path.base path);
in
- if name mem_string initiators then error (cycle_msg initiators) else ();
- if known_thy name andalso is_finished name orelse name mem_string visited then
+ if member (op =) initiators name then error (cycle_msg initiators) else ();
+ if known_thy name andalso is_finished name orelse member (op =) visited name then
(visited, (true, name))
else
let