src/HOL/simpdata.ML

--- a/src/HOL/simpdata.ML	Wed Sep 06 13:32:25 2000 +0200
+++ b/src/HOL/simpdata.ML	Wed Sep 06 16:54:12 2000 +0200
@@ -496,7 +496,7 @@
    ref_tac: int -> tactic
    the actual refutation tactic. Should be able to deal with goals
    [| A1; ...; An |] ==> False
-   where the Ai are atomic, i.e. no top-level &, | or ?
+   where the Ai are atomic, i.e. no top-level &, | or EX
 *)
 
 fun refute_tac test prep_tac ref_tac =