# HG changeset patch
# User obua
# Date 1127824775 -7200
# Node ID 94dbbffbf94be96838522e4bf9d240d20af4de23
# Parent  8ef257366a0ce6b39cf6129868d31478be65d0ae
added defs disclaimer

diff -r 8ef257366a0c -r 94dbbffbf94b src/Pure/defs.ML
--- a/src/Pure/defs.ML	Tue Sep 27 12:16:06 2005 +0200
+++ b/src/Pure/defs.ML	Tue Sep 27 14:39:35 2005 +0200
@@ -6,6 +6,10 @@
 there are no cyclic definitions. The algorithm is described in "An
 Algorithm for Determining Definitional Cycles in Higher-Order Logic
 with Overloading", Steven Obua, technical report, to be written :-)
+
+ATTENTION:
+Currently this implementation of the cylce test contains a bug of which the author is fully aware.
+This bug makes it possible to introduce inconsistent definitional cycles in Isabelle. 
 *)
 
 signature DEFS =
@@ -80,7 +84,7 @@
     (true, defs)
 
 fun checkT' (Type (a, Ts)) = Type (a, map checkT' Ts)
-  | checkT' (TFree (a, _)) = TVar ((a, 0), [])        (* FIXME !? *)
+  | checkT' (TFree (a, _)) = TVar ((a, 0), [])        
   | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), [])
   | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []);