src/HOL/Tools/sat_solver.ML

 	local
 		open PropLogic
 	in
 		fun dpll_solver fm =
 		let
-			(* We could use 'PropLogic.defcnf fm' instead of 'fm', but that   *)
-			(* sometimes introduces more boolean variables than we can handle *)
-			(* efficiently.                                                   *)
+			(* We could use 'PropLogic.defcnf fm' instead of 'nnf fm', but that *)
+			(* sometimes introduces more boolean variables than we can handle   *)
+			(* efficiently.                                                     *)
+			val fm' = PropLogic.nnf fm
 			(* int list *)
-			val indices = PropLogic.indices fm
+			val indices = PropLogic.indices fm'
 			(* int list -> int -> prop_formula *)
 			fun partial_var_eval []      i = BoolVar i
 			  | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
 			(* int list -> prop_formula -> prop_formula *)
 			fun partial_eval xs True             = True

 				if x=i then true
 				else if x=(~i) then false
 				else assignment_from_list xs i
 		in
 			(* initially, no variable is interpreted yet *)
-			apsome assignment_from_list (dpll [] fm)
+			apsome assignment_from_list (dpll [] fm')
 		end
 	end  (* local *)
 in
 	SatSolver.add_solver ("dpll", Some o dpll_solver)
 end;