Infinite chains in definitions are now detected, too.

--- a/src/Pure/defs.ML	Mon May 30 10:25:46 2005 +0200
+++ b/src/Pure/defs.ML	Mon May 30 16:32:47 2005 +0200
@@ -13,14 +13,15 @@
 
     exception DEFS of string
     exception CIRCULAR of (typ * string * string) list
+    exception INFINITE_CHAIN of (typ * string * string) list 
     exception CLASH of string * string * string
     
     val empty : graph
     val declare : graph -> string -> typ -> graph  (* exception DEFS *)
-    val define : graph -> string -> typ -> string -> (string * typ) list -> graph (* exception DEFS, CIRCULAR, CLASH *)
+    val define : graph -> string -> typ -> string -> (string * typ) list -> graph (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH *)
 
     (* the first argument should be the smaller graph *)
-    val merge : graph -> graph -> graph (* exception CIRCULAR, CLASH *)
+    val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
 
 end
 
@@ -70,6 +71,7 @@
 
 exception DEFS of string;
 exception CIRCULAR of (typ * string * string) list;
+exception INFINITE_CHAIN of (typ * string * string) list;
 exception CLASH of string * string * string;
 
 fun def_err s = raise (DEFS s)
@@ -390,7 +392,13 @@
 				    val _ = 
 					if noderef = mainref andalso defname = axname then
 					    (case unify alpha' ty' of
-						 NONE => ()
+						 NONE => 
+						   if (is_instance_r ty' alpha') then
+						       raise (INFINITE_CHAIN (
+							      (alpha', mainref, axname)::
+							      (subst_history s_beta history)@
+							      [(ty', mainref, axname)]))
+						   else ()
 					       | SOME s => raise (CIRCULAR (
 								  (subst s alpha', mainref, axname)::
 								  (subst_history s (subst_history s_beta history))@

--- a/src/Pure/theory.ML	Mon May 30 10:25:46 2005 +0200
+++ b/src/Pure/theory.ML	Mon May 30 16:32:47 2005 +0200
@@ -396,14 +396,18 @@
 
 fun pretty_const sg (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
 
-fun cycle_msg sg namess = Pretty.string_of (Pretty.block (((Pretty.str "cyclic dependency found: ") :: Pretty.fbrk :: (
-  let      
-      fun f last (ty, constname, defname) =  
-	  (pretty_const sg (constname, ty)) @ (if last then [] else [Pretty.str (" depends via "^ quote defname^ " on ")])
+fun cycle_msg sg (infinite, namess) = 
+  let val header = if not (infinite) then "cyclic dependency found: " else "infinite chain found: "
+  in
+      Pretty.string_of (Pretty.block (((Pretty.str header) :: Pretty.fbrk :: (
+        let      
+	    fun f last (ty, constname, defname) =  
+		(pretty_const sg (constname, ty)) @ (if last then [] else [Pretty.str (" depends via "^ quote defname^ " on ")])
           	
-  in
-      foldr (fn (x,r) => (f (r=[]) x)@[Pretty.fbrk]@r) [] namess
-  end))))
+	in
+	    foldr (fn (x,r) => (f (r=[]) x)@[Pretty.fbrk]@r) [] namess
+	end))))
+  end
 
 fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
   let
@@ -455,7 +459,8 @@
 	 let 
 	     val deps' = Defs.define deps c ty name body
 		 handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s) 
-		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg s)
+		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg (false, s))
+                      | Defs.INFINITE_CHAIN s => err_in_defn sg name (cycle_msg sg (true, s)) 
                       | Defs.CLASH (_, def1, def2) => err_in_defn sg name (
 			  "clashing definitions "^ quote def1 ^" and "^ quote def2)
 	 in
@@ -565,7 +570,8 @@
 
     val depss = map (#const_deps o rep_theory) thys;
     val deps' = foldl (uncurry Defs.merge) (hd depss) (tl depss)
-      handle Defs.CIRCULAR namess => error (cycle_msg sign' namess);
+      handle Defs.CIRCULAR namess => error (cycle_msg sign' (false, namess))
+	   | Defs.INFINITE_CHAIN namess => error (cycle_msg sign' (true, namess))
 
     val final_constss = map (#final_consts o rep_theory) thys;
     val final_consts' =