src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Thu Sep 02 11:02:13 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 02 11:29:02 2010 +0200
@@ -32,6 +32,7 @@
   ("Tools/recfun_codegen.ML")
   "Tools/async_manager.ML"
   "Tools/try.ML"
+  ("Tools/cnf_funcs.ML")
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -1645,7 +1646,6 @@
   "(\<not> \<not>(P)) = P"
 by blast+
 
-
 subsection {* Basic ML bindings *}
 
 ML {*
@@ -1699,6 +1699,7 @@
 val trans = @{thm trans}
 *}
 
+use "Tools/cnf_funcs.ML"
 
 subsection {* Code generator setup *}