diff -r 95b8afcbb0ed -r 6c394343360f src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Mon Jul 27 20:45:40 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Mon Jul 27 23:17:40 2009 +0200
@@ -33,19 +33,20 @@
 
 signature CNF =
 sig
-	val is_atom           : Term.term -> bool
-	val is_literal        : Term.term -> bool
-	val is_clause         : Term.term -> bool
-	val clause_is_trivial : Term.term -> bool
+	val is_atom: term -> bool
+	val is_literal: term -> bool
+	val is_clause: term -> bool
+	val clause_is_trivial: term -> bool
 
-	val clause2raw_thm : Thm.thm -> Thm.thm
+	val clause2raw_thm: thm -> thm
 
-	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
+	val weakening_tac: int -> tactic  (* removes the first hypothesis of a subgoal *)
 
-	val make_cnf_thm  : theory -> Term.term -> Thm.thm
-	val make_cnfx_thm : theory -> Term.term ->  Thm.thm
-	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
-	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
+	val make_cnf_thm: theory -> term -> thm
+	val make_cnfx_thm: theory -> term -> thm
+	val cnf_rewrite_tac: Proof.context -> int -> tactic  (* converts all prems of a subgoal to CNF *)
+	val cnfx_rewrite_tac: Proof.context -> int -> tactic
+	  (* converts all prems of a subgoal to (almost) definitional CNF *)
 end;
 
 structure cnf : CNF =
@@ -505,8 +506,6 @@
 (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
 (* ------------------------------------------------------------------------- *)
 
-(* int -> Tactical.tactic *)
-
 fun weakening_tac i =
 	dtac weakening_thm i THEN atac (i+1);
 
@@ -516,17 +515,16 @@
 (*      premise)                                                             *)
 (* ------------------------------------------------------------------------- *)
 
-(* int -> Tactical.tactic *)
-
-fun cnf_rewrite_tac i =
+fun cnf_rewrite_tac ctxt i =
 	(* cut the CNF formulas as new premises *)
-	OldGoals.METAHYPS (fn prems =>
+	FOCUS (fn {prems, ...} =>
 		let
-			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
+		  val thy = ProofContext.theory_of ctxt
+			val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
 			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
 		in
 			cut_facts_tac cut_thms 1
-		end) i
+		end) ctxt i
 	(* remove the original premises *)
 	THEN SELECT_GOAL (fn thm =>
 		let
@@ -540,17 +538,16 @@
 (*      (possibly introducing new literals)                                  *)
 (* ------------------------------------------------------------------------- *)
 
-(* int -> Tactical.tactic *)
-
-fun cnfx_rewrite_tac i =
+fun cnfx_rewrite_tac ctxt i =
 	(* cut the CNF formulas as new premises *)
-	OldGoals.METAHYPS (fn prems =>
+	FOCUS (fn {prems, ...} =>
 		let
-			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
+		  val thy = ProofContext.theory_of ctxt;
+			val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
 			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
 		in
 			cut_facts_tac cut_thms 1
-		end) i
+		end) ctxt i
 	(* remove the original premises *)
 	THEN SELECT_GOAL (fn thm =>
 		let