src/HOL/ex/cla.ML

--- a/src/HOL/ex/cla.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/ex/cla.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -381,7 +381,7 @@
   the type constraint ensures that x,y,z have the same type as a,b,u. *)
 goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
 \               --> (! u::'a. P(u))";
-by (Classical.safe_tac (claset()));
+by (Classical.Safe_tac);
 by (res_inst_tac [("x","a")] allE 1);
 by (assume_tac 1);
 by (res_inst_tac [("x","b")] allE 1);