diff -r 575bd6548df9 -r b22e44496dc2 src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Tue Oct 20 16:13:01 2009 +0200
@@ -111,8 +111,8 @@
 	  | indices False            = []
 	  | indices (BoolVar i)      = [i]
 	  | indices (Not fm)         = indices fm
-	  | indices (Or (fm1, fm2))  = (indices fm1) union_int (indices fm2)
-	  | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
+	  | indices (Or (fm1, fm2))  = gen_union (op =) (indices fm1, indices fm2)
+	  | indices (And (fm1, fm2)) = gen_union (op =) (indices fm1, indices fm2);
 
 (* ------------------------------------------------------------------------- *)
 (* maxidx: computes the maximal variable index occuring in a formula of      *)