src/HOL/Nominal/nominal_inductive2.ML
changeset 33040 cffdb7b28498
parent 33038 8f9594c31de4
child 33049 c38f02fdf35d
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 08:16:25 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 10:15:31 2009 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4      val elims = map (atomize_induct ctxt) elims;
     1.5      val monos = Inductive.get_monos ctxt;
     1.6      val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     1.7 -    val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
     1.8 +    val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
     1.9          [] => ()
    1.10        | xs => error ("Missing equivariance theorem for predicate(s): " ^
    1.11            commas_quote xs));
    1.12 @@ -176,7 +176,7 @@
    1.13      val _ = (case duplicates (op = o pairself fst) avoids of
    1.14          [] => ()
    1.15        | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
    1.16 -    val _ = (case map fst avoids \\ induct_cases of
    1.17 +    val _ = (case subtract (op =) induct_cases (map fst avoids) of
    1.18          [] => ()
    1.19        | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
    1.20      fun mk_avoids params name sets =
    1.21 @@ -300,7 +300,7 @@
    1.22      val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
    1.23      val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
    1.24      val dj_thms = maps (fn a =>
    1.25 -      map (NominalAtoms.dj_thm_of thy a) (atoms \ a)) atoms;
    1.26 +      map (NominalAtoms.dj_thm_of thy a) (remove (op =) a atoms)) atoms;
    1.27      val finite_ineq = map2 (fn th => fn th' => th' RS (th RS
    1.28        @{thm pt_set_finite_ineq})) pt_insts at_insts;
    1.29      val perm_set_forget =