1.1 --- a/src/HOL/Tools/refute.ML	Fri Apr 16 20:33:16 2004 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Apr 16 20:34:41 2004 +0200
     1.3 @@ -210,11 +210,10 @@
     1.4  	fun is_satisfying_model model intr satisfy =
     1.5  	let
     1.6  		(* prop_formula list -> prop_formula *)
     1.7 -		fun allfalse []      = True
     1.8 -		  | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
     1.9 +		fun oneoutoftwofalse []      = True
    1.10 +		  | oneoutoftwofalse (x::xs) = SAnd (PropLogic.all (map (fn x' => SOr (SNot x, SNot x')) xs), oneoutoftwofalse xs)
    1.11  		(* prop_formula list -> prop_formula *)
    1.12 -		fun exactly1true []      = False
    1.13 -		  | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
    1.14 +		fun exactly1true xs = SAnd (PropLogic.exists xs, oneoutoftwofalse xs)
    1.15  	(* ------------------------------------------------------------------------- *)
    1.16  	(* restrict_to_single_element: returns a propositional formula that is true  *)
    1.17  	(*      iff the interpretation denotes a single element of its corresponding *)