src/HOL/Induct/Acc.ML

--- a/src/HOL/Induct/Acc.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Acc.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -18,7 +18,7 @@
                             map (rewrite_rule [pred_def]) acc.intrs)) 1);
 qed "accI";
 
-Goal "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
+Goal "[| b: acc(r);  (a,b): r |] ==> a: acc(r)";
 by (etac acc.elim 1);
 by (rewtac pred_def);
 by (Fast_tac 1);