# HG changeset patch
# User webertj
# Date 1082140481 -7200
# Node ID 1946097f706883da1516f48db99623f141455e74
# Parent  985eb6708207b1fb7eea41fc7a8788bd97a3bea1
exactly1true rewritten (much better when converting to CNF now)

diff -r 985eb6708207 -r 1946097f7068 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Apr 16 20:33:16 2004 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Apr 16 20:34:41 2004 +0200
@@ -210,11 +210,10 @@
 	fun is_satisfying_model model intr satisfy =
 	let
 		(* prop_formula list -> prop_formula *)
-		fun allfalse []      = True
-		  | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
+		fun oneoutoftwofalse []      = True
+		  | oneoutoftwofalse (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), oneoutoftwofalse xs)
 		(* prop_formula list -> prop_formula *)
-		fun exactly1true []      = False
-		  | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
+		fun exactly1true xs = SAnd (PropLogic.exists xs, oneoutoftwofalse xs)
 	(* ------------------------------------------------------------------------- *)
 	(* restrict_to_single_element: returns a propositional formula that is true  *)
 	(*      iff the interpretation denotes a single element of its corresponding *)