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