src/HOL/ex/cla.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4353 d565d2197a5f
     1.1 --- a/src/HOL/ex/cla.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/ex/cla.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -381,7 +381,7 @@
     1.4    the type constraint ensures that x,y,z have the same type as a,b,u. *)
     1.5  goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
     1.6  \               --> (! u::'a. P(u))";
     1.7 -by (Classical.safe_tac (claset()));
     1.8 +by (Classical.Safe_tac);
     1.9  by (res_inst_tac [("x","a")] allE 1);
    1.10  by (assume_tac 1);
    1.11  by (res_inst_tac [("x","b")] allE 1);