diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Oct 21 10:15:31 2009 +0200
@@ -240,7 +240,7 @@
               if is_some (covering g true j) then SOME (j, b) else NONE
             fun get_wk_cover (j, b) = the (covering g false j)
 
-            val qs = lq \\ map_filter get_str_cover lq
+            val qs = subtract (op =) (map_filter get_str_cover lq) lq
             val ps = map get_wk_cover qs
 
             fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
@@ -263,7 +263,8 @@
             THEN EVERY (map2 (less_proof false) qs ps)
             THEN (if strict orelse qs <> lq
                   then LocalDefs.unfold_tac ctxt set_of_simps
-                       THEN steps_tac MAX true (lq \\ qs) (lp \\ ps)
+                       THEN steps_tac MAX true
+                       (subtract (op =) qs lq) (subtract (op =) ps lp)
                   else all_tac)
           end
       in
@@ -296,7 +297,7 @@
            (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
          THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
          THEN EVERY (map (prove_lev true) sl)
-         THEN EVERY (map (prove_lev false) ((0 upto length cs - 1) \\ sl)))
+         THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
     end