src/ZF/ZF.ML

--- a/src/ZF/ZF.ML	Thu Jan 19 19:46:49 1995 +0100
+++ b/src/ZF/ZF.ML	Fri Jan 20 02:00:23 1995 +0100
@@ -405,7 +405,7 @@
 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
  (fn _ => [REPEAT (ares_tac [notI, equals0D] 1)]);
 
-qed_goal "not_emptyE" ZF.thy "[| A ~= 0;  !!x. x:A ==> R |] ==> R";
+qed_goal "not_emptyE" ZF.thy "[| A ~= 0;  !!x. x:A ==> R |] ==> R"
  (fn [major,minor]=>
   [ rtac ([major, equals0I] MRS swap) 1,
     swap_res_tac [minor] 1,