--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 08:16:25 2009 +0200
@@ -984,20 +984,20 @@
val dupTs = map snd (duplicates (op =) vTs) @
map_filter (AList.lookup (op =) vTs) vs;
in
- terms_vs (in_ts @ in_ts') subset vs andalso
+ subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
forall (is_eqT o fastype_of) in_ts' andalso
- term_vs t subset vs andalso
+ subset (op =) (term_vs t, vs) andalso
forall is_eqT dupTs
end)
(modes_of_term modes t handle Option =>
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
| Negprem (us, t) => find_first (fn Mode (_, is, _) =>
length us = length is andalso
- terms_vs us subset vs andalso
- term_vs t subset vs)
+ subset (op =) (terms_vs us, vs) andalso
+ subset (op =) (term_vs t, vs))
(modes_of_term modes t handle Option =>
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
- | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
+ | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
else NONE
) ps);
@@ -1047,16 +1047,16 @@
(if with_generator then
(case select_mode_prem thy gen_modes' vs ps of
SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps)
- (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
+ (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
(filter_out (equal p) ps)
| _ =>
let
val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
in
case (find_first (fn generator_vs => is_some
- (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
+ (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
- (vs union generator_vs) ps
+ (union (op =) (vs, generator_vs)) ps
| NONE => let
val _ = tracing ("ps:" ^ (commas
(map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
@@ -1065,7 +1065,7 @@
else
NONE)
| SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps)
- (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
+ (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
(filter_out (equal p) ps))
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
val in_vs = terms_vs in_ts;
@@ -1073,13 +1073,13 @@
in
if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
forall (is_eqT o fastype_of) in_ts' then
- case check_mode_prems [] (param_vs union in_vs) ps of
+ case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of
NONE => NONE
| SOME (acc_ps, vs) =>
if with_generator then
SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs)))
else
- if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
+ if subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
else NONE
end;