diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/prop_logic.ML	Wed Oct 21 08:16:25 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))  = union (op =) (indices fm1, indices fm2)
+	  | indices (And (fm1, fm2)) = union (op =) (indices fm1, indices fm2);
 
 (* ------------------------------------------------------------------------- *)
 (* maxidx: computes the maximal variable index occuring in a formula of      *)