the_equality [intro];

--- a/src/HOL/cladata.ML	Sun Jul 22 21:30:21 2001 +0200
+++ b/src/HOL/cladata.ML	Sun Jul 22 21:31:00 2001 +0200
@@ -66,7 +66,7 @@
                        addSEs [conjE,disjE,impCE,FalseE,iffCE];
 
 (*Quantifier rules*)
-val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality] 
+val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality, the_equality] 
                      addSEs [exE] addEs [allE];
 
 val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];