src/HOL/Tools/cnf_funcs.ML
changeset 32283 3bebc195c124
parent 32232 6c394343360f
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Thu Jul 30 11:23:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Thu Jul 30 12:20:43 2009 +0200
     1.3 @@ -517,7 +517,7 @@
     1.4  
     1.5  fun cnf_rewrite_tac ctxt i =
     1.6  	(* cut the CNF formulas as new premises *)
     1.7 -	FOCUS (fn {prems, ...} =>
     1.8 +	Subgoal.FOCUS (fn {prems, ...} =>
     1.9  		let
    1.10  		  val thy = ProofContext.theory_of ctxt
    1.11  			val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
    1.12 @@ -540,7 +540,7 @@
    1.13  
    1.14  fun cnfx_rewrite_tac ctxt i =
    1.15  	(* cut the CNF formulas as new premises *)
    1.16 -	FOCUS (fn {prems, ...} =>
    1.17 +	Subgoal.FOCUS (fn {prems, ...} =>
    1.18  		let
    1.19  		  val thy = ProofContext.theory_of ctxt;
    1.20  			val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems