src/ZF/ex/enum.ML

--- a/src/ZF/ex/enum.ML	Thu Oct 07 10:48:16 1993 +0100
+++ b/src/ZF/ex/enum.ML	Thu Oct 07 11:47:50 1993 +0100
@@ -27,7 +27,7 @@
   val type_intrs = data_typechecks
   val type_elims = []);
 
-goal Enum.thy "~ con59=con60";
+goal Enum.thy "con59 ~= con60";
 by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);  (*2.3 secs*)
 result();