author | obua |

Tue Sep 27 14:39:35 2005 +0200 (2005-09-27) | |

changeset 17669 | 94dbbffbf94b |

parent 17668 | 8ef257366a0c |

child 17670 | bf4f2c1b26cc |

added defs disclaimer

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