src/HOL/Tools/inductive_codegen.ML
changeset 33037 b22e44496dc2
parent 32957 675c0c7e6a37
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -202,15 +202,15 @@
     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              (if is_set then [Mode (([], []), [], [])]
    1.15               else modes_of modes t handle Option =>
    1.16                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
    1.17 -      | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
    1.18 +      | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
    1.19            else NONE) ps);
    1.20  
    1.21  fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
    1.22 @@ -222,7 +222,7 @@
    1.23        | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
    1.24            NONE => NONE
    1.25          | SOME (x, _) => check_mode_prems
    1.26 -            (case x of Prem (us, _, _) => vs union terms_vs us | _ => vs)
    1.27 +            (case x of Prem (us, _, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
    1.28              (filter_out (equal x) ps));
    1.29      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
    1.30      val in_vs = terms_vs in_ts;
    1.31 @@ -230,9 +230,9 @@
    1.32    in
    1.33      forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
    1.34      forall (is_eqT o fastype_of) in_ts' andalso
    1.35 -    (case check_mode_prems (arg_vs union in_vs) ps of
    1.36 +    (case check_mode_prems (gen_union (op =) (arg_vs, in_vs)) ps of
    1.37         NONE => false
    1.38 -     | SOME vs => concl_vs subset vs)
    1.39 +     | SOME vs => gen_subset (op =) (concl_vs, vs))
    1.40    end;
    1.41  
    1.42  fun check_modes_pred thy arg_vs preds modes (p, ms) =
    1.43 @@ -482,7 +482,7 @@
    1.44  fun constrain cs [] = []
    1.45    | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
    1.46        NONE => xs
    1.47 -    | SOME xs' => xs inter xs') :: constrain cs ys;
    1.48 +    | SOME xs' => gen_inter (op =) (xs, xs')) :: constrain cs ys;
    1.49  
    1.50  fun mk_extra_defs thy defs gr dep names module ts =
    1.51    Library.foldl (fn (gr, name) =>