# HG changeset patch
# User wenzelm
# Date 1416856011 -3600
# Node ID 376446e98951918828d696354d496a92037a9aa2
# Parent  7dc8ac6f089528d216d5df4e4f2e5cb6317017f5
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;

diff -r 7dc8ac6f0895 -r 376446e98951 src/Pure/defs.ML
--- 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" "";