--- a/src/HOL/Metis.thy Tue Oct 05 11:14:56 2010 +0200
+++ b/src/HOL/Metis.thy Tue Oct 05 11:45:10 2010 +0200
@@ -31,4 +31,7 @@
use "Tools/Metis/metis_tactics.ML"
setup Metis_Tactics.setup
+hide_const (open) fequal
+hide_fact (open) fequal_imp_equal equal_imp_fequal equal_imp_equal
+
end