added defs disclaimer
authorobua
Tue Sep 27 14:39:35 2005 +0200 (2005-09-27)
changeset 1766994dbbffbf94b
parent 17668 8ef257366a0c
child 17670 bf4f2c1b26cc
added defs disclaimer
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Tue Sep 27 12:16:06 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Tue Sep 27 14:39:35 2005 +0200
     1.3 @@ -6,6 +6,10 @@
     1.4  there are no cyclic definitions. The algorithm is described in "An
     1.5  Algorithm for Determining Definitional Cycles in Higher-Order Logic
     1.6  with Overloading", Steven Obua, technical report, to be written :-)
     1.7 +
     1.8 +ATTENTION:
     1.9 +Currently this implementation of the cylce test contains a bug of which the author is fully aware.
    1.10 +This bug makes it possible to introduce inconsistent definitional cycles in Isabelle. 
    1.11  *)
    1.12  
    1.13  signature DEFS =
    1.14 @@ -80,7 +84,7 @@
    1.15      (true, defs)
    1.16  
    1.17  fun checkT' (Type (a, Ts)) = Type (a, map checkT' Ts)
    1.18 -  | checkT' (TFree (a, _)) = TVar ((a, 0), [])        (* FIXME !? *)
    1.19 +  | checkT' (TFree (a, _)) = TVar ((a, 0), [])        
    1.20    | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), [])
    1.21    | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []);
    1.22