src/HOL/ex/predicate_compile.ML
changeset 33037 b22e44496dc2
parent 33004 715566791eb0
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/ex/predicate_compile.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -908,20 +908,20 @@
     1.4              val dupTs = map snd (duplicates (op =) vTs) @
     1.5                map_filter (AList.lookup (op =) vTs) vs;
     1.6            in
     1.7 -            terms_vs (in_ts @ in_ts') subset vs andalso
     1.8 +            gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
     1.9              forall (is_eqT o fastype_of) in_ts' andalso
    1.10 -            term_vs t subset vs andalso
    1.11 +            gen_subset (op =) (term_vs t, vs) andalso
    1.12              forall is_eqT dupTs
    1.13            end)
    1.14              (modes_of_term modes t handle Option =>
    1.15                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
    1.16        | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
    1.17              length us = length is andalso
    1.18 -            terms_vs us subset vs andalso
    1.19 -            term_vs t subset vs)
    1.20 +            gen_subset (op =) (terms_vs us, vs) andalso
    1.21 +            gen_subset (op =) (term_vs t, vs)
    1.22              (modes_of_term modes t handle Option =>
    1.23                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
    1.24 -      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
    1.25 +      | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
    1.26            else NONE
    1.27        ) ps);
    1.28  
    1.29 @@ -964,22 +964,22 @@
    1.30              (if with_generator then
    1.31                (case select_mode_prem thy gen_modes' vs ps of
    1.32                    SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
    1.33 -                  (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
    1.34 +                  (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
    1.35                    (filter_out (equal p) ps)
    1.36                  | NONE =>
    1.37                    let 
    1.38                      val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
    1.39                    in
    1.40                      case (find_first (fn generator_vs => is_some
    1.41 -                      (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
    1.42 +                      (select_mode_prem thy modes' (gen_union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
    1.43                        SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
    1.44 -                        (vs union generator_vs) ps
    1.45 +                        (gen_union (op =) (vs, generator_vs)) ps
    1.46                      | NONE => NONE
    1.47                    end)
    1.48              else
    1.49                NONE)
    1.50          | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
    1.51 -            (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
    1.52 +            (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
    1.53              (filter_out (equal p) ps))
    1.54      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
    1.55      val in_vs = terms_vs in_ts;
    1.56 @@ -987,13 +987,13 @@
    1.57    in
    1.58      if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
    1.59      forall (is_eqT o fastype_of) in_ts' then
    1.60 -      case check_mode_prems [] (param_vs union in_vs) ps of
    1.61 +      case check_mode_prems [] (gen_union (op =) (param_vs, in_vs)) ps of
    1.62           NONE => NONE
    1.63         | SOME (acc_ps, vs) =>
    1.64           if with_generator then
    1.65             SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
    1.66           else
    1.67 -           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
    1.68 +           if gen_subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
    1.69      else NONE
    1.70    end;
    1.71