# HG changeset patch
# User wenzelm
# Date 1026986925 -7200
# Node ID c48c634605f101c6d4f9be93249879f9e1d30aa4
# Parent  0cbda884a7e5e75b7c4e41a22f35473032585d56
ACe_axioms;

diff -r 0cbda884a7e5 -r c48c634605f1 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jul 18 12:05:51 2002 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Jul 18 12:08:45 2002 +0200
@@ -720,7 +720,7 @@
     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   apply (induct set: Finites)
    apply simp
-  apply (simp add: AC ACe.axioms ACe_axioms_def
+  apply (simp add: AC ACe_axioms ACe_axioms_def
     LC_axioms_def LC.fold_insert insert_absorb Int_insert_left)
   done