src/HOL/Metis_Examples/BigO.thy

--- a/src/HOL/Metis_Examples/BigO.thy	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Metis_Examples/BigO.thy	Thu Mar 24 17:49:27 2011 +0100
@@ -15,6 +15,8 @@
   "~~/src/HOL/Library/Set_Algebras"
 begin
 
+declare [[metis_new_skolemizer]]
+
 subsection {* Definitions *}
 
 definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set"    ("(1O'(_'))") where