diff -r d13addf9101e -r 79b37d5e50b1 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Jun 07 17:13:58 2005 +0200
+++ b/src/Pure/theory.ML	Tue Jun 07 20:04:41 2005 +0200
@@ -393,12 +393,16 @@
    | prts => Pretty.block (pretty_const pp (c, T) @
       [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
 
+fun chain_history_msg s = 
+    if Defs.chain_history () then s^": " 
+    else s^" (set DEFS_CHAIN_HISTORY=ON for full history): "
+
 fun defs_circular pp path =
-  Pretty.str "Cyclic dependency in definitions: " :: pretty_path pp path
+  Pretty.str (chain_history_msg "Cyclic dependency of definitions") :: pretty_path pp path
   |> Pretty.chunks |> Pretty.string_of;
 
 fun defs_infinite_chain pp path =
-  Pretty.str "Infinite chain in definitions: " :: pretty_path pp path
+  Pretty.str (chain_history_msg "Infinite chain of definitions") :: pretty_path pp path
   |> Pretty.chunks |> Pretty.string_of;
 
 fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;