diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -258,7 +258,7 @@
 
 fun make_under_quantifiers ctxt make t =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     fun conv ctxt ct =
       case term_of ct of
         (t1 as Const _) $ (t2 as Abs _) =>
@@ -269,7 +269,7 @@
   in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end
 
 fun make_nnf_thm_under_quantifiers ctxt =
-  make_under_quantifiers ctxt (make_nnf_thm (ProofContext.theory_of ctxt))
+  make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
 
 (* ------------------------------------------------------------------------- *)
 (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
@@ -344,7 +344,7 @@
 
 fun make_cnf_thm ctxt t =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
           let
             val thm1 = make_cnf_thm_from_nnf x
@@ -414,7 +414,7 @@
 
 fun make_cnfx_thm ctxt t =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val var_id = Unsynchronized.ref 0  (* properly initialized below *)
     fun new_free () =
       Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)