# HG changeset patch
# User wenzelm
# Date 963523568 -7200
# Node ID ff3a86a00ea541f892db5c2eb1ef829a0de8b7ac
# Parent  3da45f19730e4c54f04364290261dac014304f6b
tuned cycle_msg;

diff -r 3da45f19730e -r ff3a86a00ea5 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Jul 13 23:23:24 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Jul 13 23:26:08 2000 +0200
@@ -76,13 +76,13 @@
 fun loader_msg txt names = gen_msg ("Theory loader: " ^ txt) names;
 
 val show_path = space_implode " via " o map quote;
-fun cycle_msg name names = loader_msg ("cyclic dependency of " ^ show_path (name :: names)) [];
+fun cycle_msg names = loader_msg ("cyclic dependency of " ^ show_path names) [];
 
 
 (* derived graph operations *)
 
 fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G
-  handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess));
+  handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
 
 fun upd_deps name entry G =
   foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name)
@@ -311,7 +311,7 @@
     val path = Path.expand (Path.unpack str);
     val name = Path.pack (Path.base path);
   in
-    if name mem_string initiators then error (cycle_msg name initiators) else ();
+    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
       (visited, (true, name))
     else
diff -r 3da45f19730e -r ff3a86a00ea5 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Jul 13 23:23:24 2000 +0200
+++ b/src/Pure/theory.ML	Thu Jul 13 23:26:08 2000 +0200
@@ -377,8 +377,8 @@
   (error_msg msg;
     error ("The error(s) above occurred in definition " ^ quote (Sign.full_name sg name)));
 
-fun cycle_msg namess =
-  "Cyclic dependency of constants:\n" ^ cat_lines (map (space_implode " -> " o map quote) namess);
+fun cycle_msg namess = "Cyclic dependency of constants:\n" ^
+  cat_lines (map (space_implode " -> " o map quote o rev) namess);
 
 fun add_deps (c, cs) deps =
   let fun declare (G, x) = Graph.new_node (x, ()) G handle Graph.DUP _ => G