src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 33037 b22e44496dc2
parent 33004 715566791eb0
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -984,20 +984,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 @@ -1047,16 +1047,16 @@
    1.30              (if with_generator then
    1.31                (case select_mode_prem thy gen_modes' vs ps of
    1.32                  SOME (p as Prem _, 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                | _ =>
    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 => let
    1.47                      val _ = tracing ("ps:" ^ (commas
    1.48                      (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
    1.49 @@ -1065,7 +1065,7 @@
    1.50              else
    1.51                NONE)
    1.52          | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
    1.53 -            (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
    1.54 +            (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
    1.55              (filter_out (equal p) ps))
    1.56      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
    1.57      val in_vs = terms_vs in_ts;
    1.58 @@ -1073,13 +1073,13 @@
    1.59    in
    1.60      if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
    1.61      forall (is_eqT o fastype_of) in_ts' then
    1.62 -      case check_mode_prems [] (param_vs union in_vs) ps of
    1.63 +      case check_mode_prems [] (gen_union (op =) (param_vs, in_vs)) ps of
    1.64           NONE => NONE
    1.65         | SOME (acc_ps, vs) =>
    1.66           if with_generator then
    1.67             SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
    1.68           else
    1.69 -           if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
    1.70 +           if gen_subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
    1.71      else NONE
    1.72    end;
    1.73