--- a/src/HOL/HOL.thy Sun Oct 14 22:07:01 2001 +0200
+++ b/src/HOL/HOL.thy Sun Oct 14 22:08:29 2001 +0200
@@ -237,6 +237,7 @@
use "cladata.ML"
setup hypsubst_setup
+declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify]
setup Classical.setup
setup clasetup