hide "ext" name, but keep "HOL.ext", to ensure consistency in naming when "ext" is used by LEO-II or Satallax implicitly

--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Feb 07 14:05:33 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Feb 07 14:05:33 2013 +0100
@@ -16,6 +16,8 @@
 
 declare [[sledgehammer_instantiate_inducts = false]]
 
+hide_fact (open) HOL.ext
+
 ML {*
 !Multithreading.max_threads
 *}