src/Pure/proofterm.ML
changeset 33037 b22e44496dc2
parent 32810 f3466a5645fa
child 33038 8f9594c31de4
     1.1 --- a/src/Pure/proofterm.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -900,8 +900,8 @@
     1.4  
     1.5  fun add_funvars Ts (vs, t) =
     1.6    if is_fun (fastype_of1 (Ts, t)) then
     1.7 -    vs union map_filter (fn Var (ixn, T) =>
     1.8 -      if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)
     1.9 +    gen_union (op =) (vs, map_filter (fn Var (ixn, T) =>
    1.10 +      if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
    1.11    else vs;
    1.12  
    1.13  fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) =
    1.14 @@ -918,7 +918,7 @@
    1.15    | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
    1.16    | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
    1.17  
    1.18 -fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q
    1.19 +fun prop_vars (Const ("==>", _) $ P $ Q) = gen_union (op =) (prop_vars P, prop_vars Q)
    1.20    | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
    1.21    | prop_vars t = (case strip_comb t of
    1.22        (Var (ixn, _), _) => [ixn] | _ => []);
    1.23 @@ -936,9 +936,9 @@
    1.24    end;
    1.25  
    1.26  fun needed_vars prop =
    1.27 -  Library.foldl (op union)
    1.28 -    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union
    1.29 -  prop_vars prop;
    1.30 +  gen_union (op =) (Library.foldl (gen_union (op =))
    1.31 +    ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))),
    1.32 +  prop_vars prop);
    1.33  
    1.34  fun gen_axm_proof c name prop =
    1.35    let
    1.36 @@ -975,7 +975,7 @@
    1.37            let
    1.38              val p as (_, is', ch', prf') = shrink ls lev prf2;
    1.39              val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
    1.40 -          in (is union is', ch orelse ch', ts',
    1.41 +          in (gen_union (op =) (is, is'), ch orelse ch', ts',
    1.42                if ch orelse ch' then prf'' %% prf' else prf)
    1.43            end
    1.44        | shrink' ls lev ts prfs (prf as prf1 % t) =
    1.45 @@ -1004,15 +1004,15 @@
    1.46              val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
    1.47              val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
    1.48                insert (op =) ixn (case AList.lookup (op =) insts ixn of
    1.49 -                  SOME (SOME t) => if is_proj t then ixns union ixns' else ixns'
    1.50 -                | _ => ixns union ixns'))
    1.51 +                  SOME (SOME t) => if is_proj t then gen_union (op =) (ixns, ixns') else ixns'
    1.52 +                | _ => gen_union (op =) (ixns, ixns')))
    1.53                    (needed prop ts'' prfs, add_npvars false true [] ([], prop));
    1.54              val insts' = map
    1.55                (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
    1.56                  | (_, x) => (false, x)) insts
    1.57            in ([], false, insts' @ map (pair false) ts'', prf) end
    1.58      and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
    1.59 -          (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs
    1.60 +          gen_union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs)
    1.61        | needed (Var (ixn, _)) (_::_) _ = [ixn]
    1.62        | needed _ _ _ = [];
    1.63    in shrink end;