# HG changeset patch
# User blanchet
# Date 1360242333 -3600
# Node ID 0f817f80bcca7b27acf4b63a6bce6ebcda57c47e
# Parent  48e82e199df16f93d0b5f54293b55dd33fb93a68
hide "ext" name, but keep "HOL.ext", to ensure consistency in naming when "ext" is used by LEO-II or Satallax implicitly

diff -r 48e82e199df1 -r 0f817f80bcca src/HOL/TPTP/MaSh_Export.thy
--- 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
 *}