diff -r b22e44496dc2 -r 8f9594c31de4 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Oct 20 16:13:01 2009 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 21 08:14:38 2009 +0200
@@ -900,7 +900,7 @@
 
 fun add_funvars Ts (vs, t) =
   if is_fun (fastype_of1 (Ts, t)) then
-    gen_union (op =) (vs, map_filter (fn Var (ixn, T) =>
+    union (op =) (vs, map_filter (fn Var (ixn, T) =>
       if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
   else vs;
 
@@ -918,7 +918,7 @@
   | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
   | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
 
-fun prop_vars (Const ("==>", _) $ P $ Q) = gen_union (op =) (prop_vars P, prop_vars Q)
+fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P, prop_vars Q)
   | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
   | prop_vars t = (case strip_comb t of
       (Var (ixn, _), _) => [ixn] | _ => []);
@@ -936,7 +936,7 @@
   end;
 
 fun needed_vars prop =
-  gen_union (op =) (Library.foldl (gen_union (op =))
+  union (op =) (Library.foldl (union (op =))
     ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))),
   prop_vars prop);
 
@@ -975,7 +975,7 @@
           let
             val p as (_, is', ch', prf') = shrink ls lev prf2;
             val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
-          in (gen_union (op =) (is, is'), ch orelse ch', ts',
+          in (union (op =) (is, is'), ch orelse ch', ts',
               if ch orelse ch' then prf'' %% prf' else prf)
           end
       | shrink' ls lev ts prfs (prf as prf1 % t) =
@@ -1004,15 +1004,15 @@
             val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
             val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
               insert (op =) ixn (case AList.lookup (op =) insts ixn of
-                  SOME (SOME t) => if is_proj t then gen_union (op =) (ixns, ixns') else ixns'
-                | _ => gen_union (op =) (ixns, ixns')))
+                  SOME (SOME t) => if is_proj t then union (op =) (ixns, ixns') else ixns'
+                | _ => union (op =) (ixns, ixns')))
                   (needed prop ts'' prfs, add_npvars false true [] ([], prop));
             val insts' = map
               (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
                 | (_, x) => (false, x)) insts
           in ([], false, insts' @ map (pair false) ts'', prf) end
     and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
-          gen_union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs)
+          union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs)
       | needed (Var (ixn, _)) (_::_) _ = [ixn]
       | needed _ _ _ = [];
   in shrink end;