removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6);
de-facto this alternative never occured in practice, but it can lead to non-termination of the check;

--- a/src/Pure/defs.ML	Mon Nov 24 12:20:14 2014 +0100
+++ b/src/Pure/defs.ML	Mon Nov 24 20:06:51 2014 +0100
@@ -132,12 +132,8 @@
 fun err ctxt (c, args) (d, Us) s1 s2 =
   error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
 
-fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
-  | contained _ _ = false;
-
 fun acyclic ctxt (c, args) (d, Us) =
   c <> d orelse
-  exists (fn U => exists (contained U) args) Us orelse
   is_none (match_args (args, Us)) orelse
   err ctxt (c, args) (d, Us) "Circular" "";