get rid of polymorphic equality in Nitpick's code + a few minor cleanups
authorblanchet
Mon Dec 14 12:30:26 2009 +0100 (2009-12-14)
changeset 341215e831d805118
parent 34120 f9920a3ddf50
child 34122 9e6326db46b4
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Mon Dec 14 12:14:12 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Dec 14 12:30:26 2009 +0100
     1.3 @@ -996,7 +996,7 @@
     1.4  (* bool -> Time.time option -> int -> int -> problem list -> outcome *)
     1.5  fun solve_any_problem overlord deadline max_threads max_solutions problems =
     1.6    let
     1.7 -    val j = find_index (equal True o #formula) problems
     1.8 +    val j = find_index (curry (op =) True o #formula) problems
     1.9      val indexed_problems = if j >= 0 then
    1.10                               [(j, nth problems j)]
    1.11                             else
     2.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Mon Dec 14 12:14:12 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Mon Dec 14 12:30:26 2009 +0100
     2.3 @@ -232,7 +232,7 @@
     2.4         | Const (@{const_name snd}, _) => raise SAME ()
     2.5         | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
     2.6         | Free (x as (_, T)) =>
     2.7 -         Rel (arity_of RRep card T, find_index (equal x) frees)
     2.8 +         Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
     2.9         | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
    2.10         | Bound j => raise SAME ()
    2.11         | Abs (_, T, t') =>
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 14 12:14:12 2009 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 14 12:30:26 2009 +0100
     3.3 @@ -133,7 +133,7 @@
     3.4      [Pretty.str (s ^ plural_s_for_list ts ^ ":"),
     3.5       Pretty.indent indent_size (Pretty.chunks
     3.6           (map2 (fn j => fn t =>
     3.7 -                   Pretty.block [t |> shorten_const_names_in_term
     3.8 +                   Pretty.block [t |> shorten_names_in_term
     3.9                                     |> Syntax.pretty_term ctxt,
    3.10                                   Pretty.str (if j = 1 then "." else ";")])
    3.11                 (length ts downto 1) ts))]
    3.12 @@ -315,7 +315,7 @@
    3.13                       (core_u :: def_us @ nondef_us)
    3.14  *)
    3.15  
    3.16 -    val unique_scope = forall (equal 1 o length o snd) cards_assigns
    3.17 +    val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
    3.18      (* typ -> bool *)
    3.19      fun is_free_type_monotonic T =
    3.20        unique_scope orelse
    3.21 @@ -331,7 +331,7 @@
    3.22          orelse is_number_type thy T
    3.23          orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
    3.24      fun is_datatype_shallow T =
    3.25 -      not (exists (equal T o domain_type o type_of) sel_names)
    3.26 +      not (exists (curry (op =) T o domain_type o type_of) sel_names)
    3.27      val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
    3.28               |> sort TermOrd.typ_ord
    3.29      val (all_dataTs, all_free_Ts) =
    3.30 @@ -375,8 +375,9 @@
    3.31      val need_incremental = Int.max (max_potential, max_genuine) >= 2
    3.32      val effective_sat_solver =
    3.33        if sat_solver <> "smart" then
    3.34 -        if need_incremental andalso
    3.35 -           not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then
    3.36 +        if need_incremental
    3.37 +           andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
    3.38 +                               sat_solver) then
    3.39            (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
    3.40                         \be used instead of " ^ quote sat_solver ^ "."));
    3.41             "SAT4J")
    3.42 @@ -418,7 +419,7 @@
    3.43          val main_j0 = offset_of_type ofs bool_T
    3.44          val (nat_card, nat_j0) = spec_of_type scope nat_T
    3.45          val (int_card, int_j0) = spec_of_type scope int_T
    3.46 -        val _ = forall (equal main_j0) [nat_j0, int_j0]
    3.47 +        val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0)
    3.48                  orelse raise BAD ("Nitpick.pick_them_nits_in_term.\
    3.49                                    \problem_for_scope", "bad offsets")
    3.50          val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
    3.51 @@ -663,7 +664,8 @@
    3.52                  let
    3.53                    val num_genuine = take max_potential lib_ps
    3.54                                      |> map (print_and_check false)
    3.55 -                                    |> filter (equal (SOME true)) |> length
    3.56 +                                    |> filter (curry (op =) (SOME true))
    3.57 +                                    |> length
    3.58                    val max_genuine = max_genuine - num_genuine
    3.59                    val max_potential = max_potential
    3.60                                        - (length lib_ps - num_genuine)
    3.61 @@ -859,8 +861,8 @@
    3.62               error "Nitpick was interrupted."
    3.63  
    3.64  (* Proof.state -> params -> bool -> term -> string * Proof.state *)
    3.65 -fun pick_nits_in_term state (params as {debug, timeout, expect, ...})
    3.66 -                      auto orig_assm_ts orig_t =
    3.67 +fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto
    3.68 +                      orig_assm_ts orig_t =
    3.69    if getenv "KODKODI" = "" then
    3.70      (if auto then ()
    3.71       else warning (Pretty.string_of (plazy install_kodkodi_message));
    3.72 @@ -878,7 +880,7 @@
    3.73      end
    3.74  
    3.75  (* Proof.state -> params -> thm -> int -> string * Proof.state *)
    3.76 -fun pick_nits_in_subgoal state params auto subgoal =
    3.77 +fun pick_nits_in_subgoal state params auto i =
    3.78    let
    3.79      val ctxt = Proof.context_of state
    3.80      val t = state |> Proof.raw_goal |> #goal |> prop_of
    3.81 @@ -888,7 +890,7 @@
    3.82      else
    3.83        let
    3.84          val assms = map term_of (Assumption.all_assms_of ctxt)
    3.85 -        val (t, frees) = Logic.goal_params t subgoal
    3.86 +        val (t, frees) = Logic.goal_params t i
    3.87        in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end
    3.88    end
    3.89  
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Dec 14 12:14:12 2009 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Dec 14 12:30:26 2009 +0100
     4.3 @@ -52,9 +52,9 @@
     4.4    val unbox_type : typ -> typ
     4.5    val string_for_type : Proof.context -> typ -> string
     4.6    val prefix_name : string -> string -> string
     4.7 +  val shortest_name : string -> string
     4.8    val short_name : string -> string
     4.9 -  val short_const_name : string -> string
    4.10 -  val shorten_const_names_in_term : term -> term
    4.11 +  val shorten_names_in_term : term -> term
    4.12    val type_match : theory -> typ * typ -> bool
    4.13    val const_match : theory -> styp * styp -> bool
    4.14    val term_match : theory -> term * term -> bool
    4.15 @@ -197,12 +197,14 @@
    4.16  (* term * term -> term *)
    4.17  fun s_conj (t1, @{const True}) = t1
    4.18    | s_conj (@{const True}, t2) = t2
    4.19 -  | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}
    4.20 -                      else HOLogic.mk_conj (t1, t2)
    4.21 +  | s_conj (t1, t2) =
    4.22 +    if t1 = @{const False} orelse t2 = @{const False} then @{const False}
    4.23 +    else HOLogic.mk_conj (t1, t2)
    4.24  fun s_disj (t1, @{const False}) = t1
    4.25    | s_disj (@{const False}, t2) = t2
    4.26 -  | s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True}
    4.27 -                      else HOLogic.mk_disj (t1, t2)
    4.28 +  | s_disj (t1, t2) =
    4.29 +    if t1 = @{const True} orelse t2 = @{const True} then @{const True}
    4.30 +    else HOLogic.mk_disj (t1, t2)
    4.31  (* term -> term -> term *)
    4.32  fun mk_exists v t =
    4.33    HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
    4.34 @@ -213,7 +215,7 @@
    4.35    | strip_connective _ t = [t]
    4.36  (* term -> term list * term *)
    4.37  fun strip_any_connective (t as (t0 $ t1 $ t2)) =
    4.38 -    if t0 mem [@{const "op &"}, @{const "op |"}] then
    4.39 +    if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
    4.40        (strip_connective t0 t, t0)
    4.41      else
    4.42        ([t], @{const Not})
    4.43 @@ -347,19 +349,24 @@
    4.44  (* string -> string -> string *)
    4.45  val prefix_name = Long_Name.qualify o Long_Name.base_name
    4.46  (* string -> string *)
    4.47 -fun short_name s = List.last (space_explode "." s) handle List.Empty => ""
    4.48 +fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
    4.49  (* string -> term -> term *)
    4.50  val prefix_abs_vars = Term.map_abs_vars o prefix_name
    4.51  (* term -> term *)
    4.52 -val shorten_abs_vars = Term.map_abs_vars short_name
    4.53 +val shorten_abs_vars = Term.map_abs_vars shortest_name
    4.54  (* string -> string *)
    4.55 -fun short_const_name s =
    4.56 +fun short_name s =
    4.57    case space_explode name_sep s of
    4.58      [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
    4.59 -  | ss => map short_name ss |> space_implode "_"
    4.60 +  | ss => map shortest_name ss |> space_implode "_"
    4.61 +(* typ -> typ *)
    4.62 +fun shorten_names_in_type (Type (s, Ts)) =
    4.63 +    Type (short_name s, map shorten_names_in_type Ts)
    4.64 +  | shorten_names_in_type T = T
    4.65  (* term -> term *)
    4.66 -val shorten_const_names_in_term =
    4.67 -  map_aterms (fn Const (s, T) => Const (short_const_name s, T) | t => t)
    4.68 +val shorten_names_in_term =
    4.69 +  map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
    4.70 +  #> map_types shorten_names_in_type
    4.71  
    4.72  (* theory -> typ * typ -> bool *)
    4.73  fun type_match thy (T1, T2) =
    4.74 @@ -371,7 +378,7 @@
    4.75  (* theory -> term * term -> bool *)
    4.76  fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
    4.77    | term_match thy (Free (s1, T1), Free (s2, T2)) =
    4.78 -    const_match thy ((short_name s1, T1), (short_name s2, T2))
    4.79 +    const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
    4.80    | term_match thy (t1, t2) = t1 aconv t2
    4.81  
    4.82  (* typ -> bool *)
    4.83 @@ -391,7 +398,7 @@
    4.84  fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
    4.85    | is_gfp_iterator_type _ = false
    4.86  val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
    4.87 -val is_boolean_type = equal prop_T orf equal bool_T
    4.88 +fun is_boolean_type T = (T = prop_T orelse T = bool_T)
    4.89  val is_integer_type =
    4.90    member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
    4.91  val is_record_type = not o null o Record.dest_recTs
    4.92 @@ -458,6 +465,14 @@
    4.93          | NONE => case T of Type (s, Ts) => Type (s, map subst Ts) | _ => T
    4.94      in subst T end
    4.95  
    4.96 +(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
    4.97 +   e.g., by adding a field to "Datatype_Aux.info". *)
    4.98 +(* string -> bool *)
    4.99 +val is_basic_datatype =
   4.100 +    member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
   4.101 +                   @{type_name nat}, @{type_name int},
   4.102 +                   "Code_Numeral.code_numeral"]
   4.103 +
   4.104  (* theory -> typ -> typ -> typ -> typ *)
   4.105  fun instantiate_type thy T1 T1' T2 =
   4.106    Same.commit (Envir.subst_type_same
   4.107 @@ -486,8 +501,11 @@
   4.108      val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
   4.109      val (co_s, co_Ts) = dest_Type co_T
   4.110      val _ =
   4.111 -      if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()
   4.112 -      else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
   4.113 +      if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts)
   4.114 +         andalso co_s <> "fun" andalso not (is_basic_datatype co_s) then
   4.115 +        ()
   4.116 +      else
   4.117 +        raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
   4.118      val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
   4.119                                     codatatypes
   4.120    in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
   4.121 @@ -516,12 +534,6 @@
   4.122            Rep_inverse = SOME Rep_inverse}
   4.123    | NONE => NONE
   4.124  
   4.125 -(* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
   4.126 -   e.g., by adding a field to "Datatype_Aux.info". *)
   4.127 -(* string -> bool *)
   4.128 -fun is_basic_datatype s =
   4.129 -    s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
   4.130 -           @{type_name nat}, @{type_name int}, "Code_Numeral.code_numeral"]
   4.131  (* theory -> string -> bool *)
   4.132  val is_typedef = is_some oo typedef_info
   4.133  val is_real_datatype = is_some oo Datatype.get_info
   4.134 @@ -568,14 +580,15 @@
   4.135  val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
   4.136  (* theory -> string -> typ -> int *)
   4.137  fun no_of_record_field thy s T1 =
   4.138 -  find_index (equal s o fst) (Record.get_extT_fields thy T1 ||> single |> op @)
   4.139 +  find_index (curry (op =) s o fst)
   4.140 +             (Record.get_extT_fields thy T1 ||> single |> op @)
   4.141  (* theory -> styp -> bool *)
   4.142  fun is_record_get thy (s, Type ("fun", [T1, _])) =
   4.143 -    exists (equal s o fst) (all_record_fields thy T1)
   4.144 +    exists (curry (op =) s o fst) (all_record_fields thy T1)
   4.145    | is_record_get _ _ = false
   4.146  fun is_record_update thy (s, T) =
   4.147    String.isSuffix Record.updateN s andalso
   4.148 -  exists (equal (unsuffix Record.updateN s) o fst)
   4.149 +  exists (curry (op =) (unsuffix Record.updateN s) o fst)
   4.150           (all_record_fields thy (body_type T))
   4.151    handle TYPE _ => false
   4.152  fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
   4.153 @@ -608,11 +621,11 @@
   4.154    end
   4.155    handle TYPE ("dest_Type", _, _) => false
   4.156  fun is_constr_like thy (s, T) =
   4.157 -  s mem [@{const_name FunBox}, @{const_name PairBox}] orelse
   4.158 +  s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
   4.159    let val (x as (s, T)) = (s, unbox_type T) in
   4.160      Refute.is_IDT_constructor thy x orelse is_record_constr x
   4.161      orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
   4.162 -    orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]
   4.163 +    orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep}
   4.164      orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
   4.165      orelse is_coconstr thy x
   4.166    end
   4.167 @@ -644,10 +657,11 @@
   4.168  fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
   4.169    case T of
   4.170      Type ("fun", _) =>
   4.171 -    boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T))
   4.172 +    (boxy = InPair orelse boxy = InFunLHS)
   4.173 +    andalso not (is_boolean_type (body_type T))
   4.174    | Type ("*", Ts) =>
   4.175 -    boxy mem [InPair, InFunRHS1, InFunRHS2]
   4.176 -    orelse (boxy mem [InExpr, InFunLHS]
   4.177 +    boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2
   4.178 +    orelse ((boxy = InExpr orelse boxy = InFunLHS)
   4.179              andalso exists (is_boxing_worth_it ext_ctxt InPair)
   4.180                             (map (box_type ext_ctxt InPair) Ts))
   4.181    | _ => false
   4.182 @@ -660,7 +674,7 @@
   4.183  and box_type ext_ctxt boxy T =
   4.184    case T of
   4.185      Type (z as ("fun", [T1, T2])) =>
   4.186 -    if not (boxy mem [InConstr, InSel])
   4.187 +    if boxy <> InConstr andalso boxy <> InSel
   4.188         andalso should_box_type ext_ctxt boxy z then
   4.189        Type (@{type_name fun_box},
   4.190              [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
   4.191 @@ -672,8 +686,8 @@
   4.192        Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
   4.193      else
   4.194        Type ("*", map (box_type ext_ctxt
   4.195 -                               (if boxy mem [InConstr, InSel] then boxy
   4.196 -                                else InPair)) Ts)
   4.197 +                          (if boxy = InConstr orelse boxy = InSel then boxy
   4.198 +                           else InPair)) Ts)
   4.199    | _ => T
   4.200  
   4.201  (* styp -> styp *)
   4.202 @@ -922,7 +936,7 @@
   4.203    let
   4.204      (* typ list -> typ -> int *)
   4.205      fun aux avoid T =
   4.206 -      (if T mem avoid then
   4.207 +      (if member (op =) avoid T then
   4.208           0
   4.209         else case T of
   4.210           Type ("fun", [T1, T2]) =>
   4.211 @@ -957,7 +971,7 @@
   4.212                  |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
   4.213                          o snd)
   4.214              in
   4.215 -              if exists (equal 0) constr_cards then 0
   4.216 +              if exists (curry (op =) 0) constr_cards then 0
   4.217                else Integer.sum constr_cards
   4.218              end)
   4.219         | _ => raise SAME ())
   4.220 @@ -989,8 +1003,8 @@
   4.221  
   4.222  (* theory -> string -> bool *)
   4.223  fun is_funky_typedef_name thy s =
   4.224 -  s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
   4.225 -         @{type_name int}]
   4.226 +  member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
   4.227 +                 @{type_name int}] s
   4.228    orelse is_frac_type thy (Type (s, []))
   4.229  (* theory -> term -> bool *)
   4.230  fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
   4.231 @@ -1063,10 +1077,11 @@
   4.232      val (built_in_nondefs, user_nondefs) =
   4.233        List.partition (is_typedef_axiom thy false) user_nondefs
   4.234        |>> append built_in_nondefs
   4.235 -    val defs = (thy |> PureThy.all_thms_of
   4.236 -                    |> filter (equal Thm.definitionK o Thm.get_kind o snd)
   4.237 -                    |> map (prop_of o snd) |> filter is_plain_definition) @
   4.238 -               user_defs @ built_in_defs
   4.239 +    val defs =
   4.240 +      (thy |> PureThy.all_thms_of
   4.241 +           |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
   4.242 +           |> map (prop_of o snd) |> filter is_plain_definition) @
   4.243 +      user_defs @ built_in_defs
   4.244    in (defs, built_in_nondefs, user_nondefs) end
   4.245  
   4.246  (* bool -> styp -> int option *)
   4.247 @@ -1111,7 +1126,7 @@
   4.248    else
   4.249      these (Symtab.lookup table s)
   4.250      |> map_filter (try (Refute.specialize_type thy x))
   4.251 -    |> filter (equal (Const x) o term_under_def)
   4.252 +    |> filter (curry (op =) (Const x) o term_under_def)
   4.253  
   4.254  (* theory -> term -> term option *)
   4.255  fun normalized_rhs_of thy t =
   4.256 @@ -1152,7 +1167,8 @@
   4.257      (* term -> bool *)
   4.258      fun is_good_arg (Bound _) = true
   4.259        | is_good_arg (Const (s, _)) =
   4.260 -        s mem [@{const_name True}, @{const_name False}, @{const_name undefined}]
   4.261 +        s = @{const_name True} orelse s = @{const_name False}
   4.262 +        orelse s = @{const_name undefined}
   4.263        | is_good_arg _ = false
   4.264    in
   4.265      case t |> strip_abs_body |> strip_comb of
   4.266 @@ -1598,9 +1614,9 @@
   4.267    let
   4.268      val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
   4.269      val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
   4.270 -    val (main, side) = List.partition (exists_Const (equal x)) prems
   4.271 +    val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
   4.272      (* term -> bool *)
   4.273 -     val is_good_head = equal (Const x) o head_of
   4.274 +     val is_good_head = curry (op =) (Const x) o head_of
   4.275    in
   4.276      if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
   4.277    end
   4.278 @@ -1693,7 +1709,7 @@
   4.279          (x as (s, _)) =
   4.280    case triple_lookup (const_match thy) wfs x of
   4.281      SOME (SOME b) => b
   4.282 -  | _ => s mem [@{const_name Nats}, @{const_name fold_graph'}]
   4.283 +  | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'}
   4.284           orelse case AList.lookup (op =) (!wf_cache) x of
   4.285                    SOME (_, wf) => wf
   4.286                  | NONE =>
   4.287 @@ -1730,7 +1746,7 @@
   4.288        | do_disjunct j t =
   4.289          case num_occs_of_bound_in_term j t of
   4.290            0 => true
   4.291 -        | 1 => exists (equal (Bound j) o head_of) (conjuncts t)
   4.292 +        | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t)
   4.293          | _ => false
   4.294      (* term -> bool *)
   4.295      fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
   4.296 @@ -1774,7 +1790,7 @@
   4.297                    t
   4.298                end
   4.299            val (nonrecs, recs) =
   4.300 -            List.partition (equal 0 o num_occs_of_bound_in_term j)
   4.301 +            List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
   4.302                             (disjuncts body)
   4.303            val base_body = nonrecs |> List.foldl s_disj @{const False}
   4.304            val step_body = recs |> map (repair_rec j)
   4.305 @@ -1923,7 +1939,7 @@
   4.306    | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
   4.307    | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
   4.308    | Type (_, Ts) =>
   4.309 -    if T mem @{typ prop} :: @{typ bool} :: @{typ unit} :: accum then
   4.310 +    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
   4.311        accum
   4.312      else
   4.313        T :: accum
   4.314 @@ -1962,7 +1978,7 @@
   4.315           andalso has_heavy_bounds_or_vars Ts level t_comb
   4.316           andalso not (loose_bvar (t_comb, level)) then
   4.317          let
   4.318 -          val (j, seen) = case find_index (equal t_comb) seen of
   4.319 +          val (j, seen) = case find_index (curry (op =) t_comb) seen of
   4.320                              ~1 => (0, t_comb :: seen)
   4.321                            | j => (j, seen)
   4.322          in (fresh_value_var Ts k (length seen) j t_comb, seen) end
   4.323 @@ -2046,7 +2062,7 @@
   4.324           (Const (x as (s, T)), args) =>
   4.325           let val arg_Ts = binder_types T in
   4.326             if length arg_Ts = length args
   4.327 -              andalso (is_constr thy x orelse s mem [@{const_name Pair}]
   4.328 +              andalso (is_constr thy x orelse s = @{const_name Pair}
   4.329                         orelse x = dest_Const @{const Suc})
   4.330                andalso (not careful orelse not (is_Var t1)
   4.331                         orelse String.isPrefix val_var_prefix
   4.332 @@ -2141,7 +2157,8 @@
   4.333      (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
   4.334         -> term -> term *)
   4.335      and aux_eq prems zs z t' t1 t2 =
   4.336 -      if not (z mem zs) andalso not (exists_subterm (equal (Var z)) t') then
   4.337 +      if not (member (op =) zs z)
   4.338 +         andalso not (exists_subterm (curry (op =) (Var z)) t') then
   4.339          aux prems zs (subst_free [(Var z, t')] t2)
   4.340        else
   4.341          aux (t1 :: prems) (Term.add_vars t1 zs) t2
   4.342 @@ -2299,8 +2316,8 @@
   4.343           (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
   4.344           if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
   4.345             aux s0 (s1 :: ss) (T1 :: Ts) t1
   4.346 -         else if quant_s = ""
   4.347 -                 andalso s0 mem [@{const_name All}, @{const_name Ex}] then
   4.348 +         else if quant_s = "" andalso (s0 = @{const_name All}
   4.349 +                                       orelse s0 = @{const_name Ex}) then
   4.350             aux s0 [s1] [T1] t1
   4.351           else
   4.352             raise SAME ()
   4.353 @@ -2330,7 +2347,8 @@
   4.354                       | cost boundss_cum_costs (j :: js) =
   4.355                         let
   4.356                           val (yeas, nays) =
   4.357 -                           List.partition (fn (bounds, _) => j mem bounds)
   4.358 +                           List.partition (fn (bounds, _) =>
   4.359 +                                              member (op =) bounds j)
   4.360                                            boundss_cum_costs
   4.361                           val yeas_bounds = big_union fst yeas
   4.362                           val yeas_cost = Integer.sum (map snd yeas)
   4.363 @@ -2339,7 +2357,7 @@
   4.364                     val js = all_permutations (index_seq 0 num_Ts)
   4.365                              |> map (`(cost (t_boundss ~~ t_costs)))
   4.366                              |> sort (int_ord o pairself fst) |> hd |> snd
   4.367 -                   val back_js = map (fn j => find_index (equal j) js)
   4.368 +                   val back_js = map (fn j => find_index (curry (op =) j) js)
   4.369                                       (index_seq 0 num_Ts)
   4.370                     val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
   4.371                                  ts
   4.372 @@ -2355,7 +2373,8 @@
   4.373                       | build ts_cum_bounds (j :: js) =
   4.374                         let
   4.375                           val (yeas, nays) =
   4.376 -                           List.partition (fn (_, bounds) => j mem bounds)
   4.377 +                           List.partition (fn (_, bounds) =>
   4.378 +                                              member (op =) bounds j)
   4.379                                            ts_cum_bounds
   4.380                             ||> map (apfst (incr_boundvars ~1))
   4.381                         in
   4.382 @@ -2548,7 +2567,7 @@
   4.383          if t = Const x then
   4.384            list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
   4.385          else
   4.386 -          let val j = find_index (equal t) fixed_params in
   4.387 +          let val j = find_index (curry (op =) t) fixed_params in
   4.388              list_comb (if j >= 0 then nth fixed_args j else t, args)
   4.389            end
   4.390    in aux [] t end
   4.391 @@ -2582,7 +2601,7 @@
   4.392                        else case term_under_def t of Const x => [x] | _ => []
   4.393        (* term list -> typ list -> term -> term *)
   4.394        fun aux args Ts (Const (x as (s, T))) =
   4.395 -          ((if not (x mem blacklist) andalso not (null args)
   4.396 +          ((if not (member (op =) blacklist x) andalso not (null args)
   4.397                 andalso not (String.isPrefix special_prefix s)
   4.398                 andalso is_equational_fun ext_ctxt x then
   4.399                let
   4.400 @@ -2607,7 +2626,8 @@
   4.401                  (* int -> term *)
   4.402                  fun var_for_bound_no j =
   4.403                    Var ((bound_var_prefix ^
   4.404 -                        nat_subscript (find_index (equal j) bound_js + 1), k),
   4.405 +                        nat_subscript (find_index (curry (op =) j) bound_js
   4.406 +                                       + 1), k),
   4.407                         nth Ts j)
   4.408                  val fixed_args_in_axiom =
   4.409                    map (curry subst_bounds
   4.410 @@ -2739,7 +2759,8 @@
   4.411                                 \coerce_term", [t']))
   4.412          | (Type (new_s, new_Ts as [new_T1, new_T2]),
   4.413             Type (old_s, old_Ts as [old_T1, old_T2])) =>
   4.414 -          if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
   4.415 +          if old_s = @{type_name fun_box} orelse old_s = @{type_name pair_box}
   4.416 +             orelse old_s = "*" then
   4.417              case constr_expand ext_ctxt old_T t of
   4.418                Const (@{const_name FunBox}, _) $ t1 =>
   4.419                if new_s = "fun" then
   4.420 @@ -2770,13 +2791,13 @@
   4.421             fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
   4.422           | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
   4.423                              \add_boxed_types_for_var", [T'], []))
   4.424 -      | _ => exists_subterm (equal (Var z)) t' ? insert (op =) T
   4.425 +      | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
   4.426      (* typ list -> typ list -> term -> indexname * typ -> typ *)
   4.427      fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
   4.428        case t of
   4.429          @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
   4.430        | Const (s0, _) $ t1 $ _ =>
   4.431 -        if s0 mem [@{const_name "=="}, @{const_name "op ="}] then
   4.432 +        if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
   4.433            let
   4.434              val (t', args) = strip_comb t1
   4.435              val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
   4.436 @@ -2855,7 +2876,8 @@
   4.437        | Const (s as @{const_name Eps}, T) => do_description_operator s T
   4.438        | Const (s as @{const_name Tha}, T) => do_description_operator s T
   4.439        | Const (x as (s, T)) =>
   4.440 -        Const (s, if s mem [@{const_name converse}, @{const_name trancl}] then
   4.441 +        Const (s, if s = @{const_name converse}
   4.442 +                     orelse s = @{const_name trancl} then
   4.443                      box_relational_operator_type T
   4.444                    else if is_built_in_const fast_descrs x
   4.445                            orelse s = @{const_name Sigma} then
   4.446 @@ -2954,7 +2976,7 @@
   4.447        |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
   4.448        |> AList.group (op =)
   4.449        |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
   4.450 -      |> map (fn (x, zs) => (x, zs |> (x mem xs) ? cons ([], [], x)))
   4.451 +      |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
   4.452      (* special -> int *)
   4.453      fun generality (js, _, _) = ~(length js)
   4.454      (* special -> special -> bool *)
   4.455 @@ -3022,7 +3044,7 @@
   4.456        case t of
   4.457          t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
   4.458        | Const (x as (s, T)) =>
   4.459 -        (if x mem xs orelse is_built_in_const fast_descrs x then
   4.460 +        (if member (op =) xs x orelse is_built_in_const fast_descrs x then
   4.461             accum
   4.462           else
   4.463             let val accum as (xs, _) = (x :: xs, axs) in
   4.464 @@ -3175,7 +3197,7 @@
   4.465      val T = unbox_type T
   4.466      val format = format |> filter (curry (op <) 0)
   4.467    in
   4.468 -    if forall (equal 1) format then
   4.469 +    if forall (curry (op =) 1) format then
   4.470        T
   4.471      else
   4.472        let
   4.473 @@ -3226,7 +3248,8 @@
   4.474                                  SOME t => do_term t
   4.475                                | NONE =>
   4.476                                  Var (nth missing_vars
   4.477 -                                         (find_index (equal j) missing_js)))
   4.478 +                                         (find_index (curry (op =) j)
   4.479 +                                                     missing_js)))
   4.480                            Ts (0 upto max_j)
   4.481             val t = do_const x' |> fst
   4.482             val format =
   4.483 @@ -3300,7 +3323,7 @@
   4.484             (t, format_term_type thy def_table formats t)
   4.485           end)
   4.486        |>> map_types (typ_subst [(@{typ bisim_iterator}, nat_T)] o unbox_type)
   4.487 -      |>> shorten_const_names_in_term |>> shorten_abs_vars
   4.488 +      |>> shorten_names_in_term |>> shorten_abs_vars
   4.489    in do_const end
   4.490  
   4.491  (* styp -> string *)
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Dec 14 12:14:12 2009 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Dec 14 12:30:26 2009 +0100
     5.3 @@ -105,7 +105,7 @@
     5.4  fun is_known_raw_param s =
     5.5    AList.defined (op =) default_default_params s
     5.6    orelse AList.defined (op =) negated_params s
     5.7 -  orelse s mem ["max", "eval", "expect"]
     5.8 +  orelse s = "max" orelse s = "eval" orelse s = "expect"
     5.9    orelse exists (fn p => String.isPrefix (p ^ " ") s)
    5.10                  ["card", "max", "iter", "box", "dont_box", "mono", "non_mono",
    5.11                   "wf", "non_wf", "format"]
    5.12 @@ -409,7 +409,7 @@
    5.13           error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
    5.14  
    5.15  (* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
    5.16 -fun pick_nits override_params auto subgoal state =
    5.17 +fun pick_nits override_params auto i state =
    5.18    let
    5.19      val thy = Proof.theory_of state
    5.20      val ctxt = Proof.context_of state
    5.21 @@ -423,26 +423,25 @@
    5.22        |> (if auto then perhaps o try
    5.23            else if debug then fn f => fn x => f x
    5.24            else handle_exceptions ctxt)
    5.25 -         (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
    5.26 -                           |>> equal "genuine")
    5.27 +         (fn (_, state) => pick_nits_in_subgoal state params auto i
    5.28 +                           |>> curry (op =) "genuine")
    5.29    in
    5.30      if auto orelse blocking then go ()
    5.31      else (Toplevel.thread true (fn () => (go (); ())); (false, state))
    5.32    end
    5.33  
    5.34 -(* (TableFun().key * string list) list option * int option
    5.35 -   -> Toplevel.transition -> Toplevel.transition *)
    5.36 -fun nitpick_trans (opt_params, opt_subgoal) =
    5.37 +(* raw_param list option * int option -> Toplevel.transition
    5.38 +   -> Toplevel.transition *)
    5.39 +fun nitpick_trans (opt_params, opt_i) =
    5.40    Toplevel.keep (K ()
    5.41 -      o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
    5.42 +      o snd o pick_nits (these opt_params) false (the_default 1 opt_i)
    5.43        o Toplevel.proof_of)
    5.44  
    5.45  (* raw_param -> string *)
    5.46  fun string_for_raw_param (name, value) =
    5.47    name ^ " = " ^ stringify_raw_param_value value
    5.48  
    5.49 -(* (TableFun().key * string) list option -> Toplevel.transition
    5.50 -   -> Toplevel.transition *)
    5.51 +(* raw_param list option -> Toplevel.transition -> Toplevel.transition *)
    5.52  fun nitpick_params_trans opt_params =
    5.53    Toplevel.theory
    5.54        (fold set_default_raw_param (these opt_params)
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Dec 14 12:14:12 2009 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Dec 14 12:30:26 2009 +0100
     6.3 @@ -82,7 +82,7 @@
     6.4  
     6.5  (* Proof.context -> bool -> string -> typ -> rep -> string *)
     6.6  fun bound_comment ctxt debug nick T R =
     6.7 -  short_const_name nick ^
     6.8 +  short_name nick ^
     6.9    (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
    6.10     else "") ^ " : " ^ string_for_rep R
    6.11  
    6.12 @@ -725,7 +725,7 @@
    6.13  (* nfa_table -> typ -> typ -> Kodkod.rel_expr list *)
    6.14  fun direct_path_rel_exprs nfa start final =
    6.15    case AList.lookup (op =) nfa final of
    6.16 -    SOME trans => map fst (filter (equal start o snd) trans)
    6.17 +    SOME trans => map fst (filter (curry (op =) start o snd) trans)
    6.18    | NONE => []
    6.19  (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> Kodkod.rel_expr *)
    6.20  and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final =
    6.21 @@ -1031,7 +1031,7 @@
    6.22                    fold (kk_or o (kk_no o to_r)) opt_arg_us
    6.23                         (kk_rel_eq (to_rep min_R u1) (to_rep min_R u2))
    6.24                  else
    6.25 -                  kk_no (kk_difference (to_rep min_R u1) (to_rep min_R u2))
    6.26 +                  kk_subset (to_rep min_R u1) (to_rep min_R u2)
    6.27                end)
    6.28           | Op2 (Eq, T, R, u1, u2) =>
    6.29             (case min_rep (rep_of u1) (rep_of u2) of
    6.30 @@ -1067,7 +1067,7 @@
    6.31                             kk_subset (kk_product r1 r2) Kodkod.Iden
    6.32                           else if not both_opt then
    6.33                             (r1, r2) |> is_opt_rep (rep_of u2) ? swap
    6.34 -                                    |> uncurry kk_difference |> kk_no
    6.35 +                                    |-> kk_subset
    6.36                           else
    6.37                             raise SAME ()
    6.38                         else
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 14 12:14:12 2009 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 14 12:30:26 2009 +0100
     7.3 @@ -60,7 +60,7 @@
     7.4       ? prefix "\<^isub>,"
     7.5  (* string -> typ -> int -> string *)
     7.6  fun atom_name prefix (T as Type (s, _)) j =
     7.7 -    prefix ^ substring (short_name s, 0, 1) ^ atom_suffix s j
     7.8 +    prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
     7.9    | atom_name prefix (T as TFree (s, _)) j =
    7.10      prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
    7.11    | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
    7.12 @@ -125,7 +125,8 @@
    7.13          $ aux T1 T2 ps $ t1 $ t2
    7.14    in aux T1 T2 o rev end
    7.15  (* term -> bool *)
    7.16 -fun is_plain_fun (Const (s, _)) = s mem [@{const_name undefined}, non_opt_name]
    7.17 +fun is_plain_fun (Const (s, _)) =
    7.18 +    (s = @{const_name undefined} orelse s = non_opt_name)
    7.19    | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
    7.20      is_plain_fun t0
    7.21    | is_plain_fun _ = false
    7.22 @@ -350,7 +351,8 @@
    7.23              val real_j = j + offset_of_type ofs T
    7.24              val constr_x as (constr_s, constr_T) =
    7.25                get_first (fn (jss, {const, ...}) =>
    7.26 -                            if [real_j] mem jss then SOME const else NONE)
    7.27 +                            if member (op =) jss [real_j] then SOME const
    7.28 +                            else NONE)
    7.29                          (discr_jsss ~~ constrs) |> the
    7.30              val arg_Ts = curried_binder_types constr_T
    7.31              val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x)
    7.32 @@ -369,7 +371,7 @@
    7.33                                          else NONE)) sel_jsss
    7.34              val uncur_arg_Ts = binder_types constr_T
    7.35            in
    7.36 -            if co andalso (T, j) mem seen then
    7.37 +            if co andalso member (op =) seen (T, j) then
    7.38                Var (var ())
    7.39              else
    7.40                let
    7.41 @@ -408,7 +410,7 @@
    7.42                in
    7.43                  if co then
    7.44                    let val var = var () in
    7.45 -                    if exists_subterm (equal (Var var)) t then
    7.46 +                    if exists_subterm (curry (op =) (Var var)) t then
    7.47                        Const (@{const_name The}, (T --> bool_T) --> T)
    7.48                        $ Abs ("\<omega>", T,
    7.49                               Const (@{const_name "op ="}, [T, T] ---> bool_T)
    7.50 @@ -449,7 +451,8 @@
    7.51            val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
    7.52            val ts2 =
    7.53              map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
    7.54 -                                       [[int_for_bool (js mem jss)]]) jss1
    7.55 +                                       [[int_for_bool (member (op =) jss js)]])
    7.56 +                jss1
    7.57          in make_fun false T1 T2 T' ts1 ts2 end
    7.58        | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
    7.59          let
    7.60 @@ -517,7 +520,7 @@
    7.61          let
    7.62            val ((head1, args1), (head2, args2)) =
    7.63              pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
    7.64 -          val max_depth = max_depth - (if T mem coTs then 1 else 0)
    7.65 +          val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
    7.66          in
    7.67            head1 = head2
    7.68            andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
    7.69 @@ -639,10 +642,12 @@
    7.70      val (eval_names, noneval_nonskolem_nonsel_names) =
    7.71        List.partition (String.isPrefix eval_prefix o nickname_of)
    7.72                       nonskolem_nonsel_names
    7.73 -      ||> filter_out (equal @{const_name bisim_iterator_max} o nickname_of)
    7.74 +      ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
    7.75 +                      o nickname_of)
    7.76      val free_names =
    7.77        map (fn x as (s, T) =>
    7.78 -              case filter (equal x o pairf nickname_of (unbox_type o type_of))
    7.79 +              case filter (curry (op =) x
    7.80 +                           o pairf nickname_of (unbox_type o type_of))
    7.81                            free_names of
    7.82                  [name] => name
    7.83                | [] => FreeName (s, T, Any)
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 14 12:14:12 2009 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 14 12:30:26 2009 +0100
     8.3 @@ -101,7 +101,7 @@
     8.4             string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2
     8.5           | CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2
     8.6           | CType (s, []) =>
     8.7 -           if s mem [@{type_name prop}, @{type_name bool}] then "o" else s
     8.8 +           if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
     8.9           | CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s
    8.10           | CRec (s, _) => "[" ^ s ^ "]") ^
    8.11          (if need_parens then ")" else "")
    8.12 @@ -125,9 +125,10 @@
    8.13                          andalso exists (could_exist_alpha_subtype alpha_T) Ts)
    8.14    | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
    8.15  (* theory -> typ -> typ -> bool *)
    8.16 -fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) =
    8.17 -    could_exist_alpha_subtype alpha_T
    8.18 -  | could_exist_alpha_sub_ctype thy alpha_T = equal alpha_T orf is_datatype thy
    8.19 +fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
    8.20 +    could_exist_alpha_subtype alpha_T T
    8.21 +  | could_exist_alpha_sub_ctype thy alpha_T T =
    8.22 +    (T = alpha_T orelse is_datatype thy T)
    8.23  
    8.24  (* ctype -> bool *)
    8.25  fun exists_alpha_sub_ctype CAlpha = true
    8.26 @@ -164,7 +165,7 @@
    8.27    | repair_ctype cache seen (CRec (z as (s, _))) =
    8.28      case AList.lookup (op =) cache z |> the of
    8.29        CRec _ => CType (s, [])
    8.30 -    | C => if C mem seen then CType (s, [])
    8.31 +    | C => if member (op =) seen C then CType (s, [])
    8.32             else repair_ctype cache (C :: seen) C
    8.33  
    8.34  (* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *)
    8.35 @@ -490,7 +491,7 @@
    8.36  
    8.37  (* literal list -> unit *)
    8.38  fun print_solution lits =
    8.39 -  let val (pos, neg) = List.partition (equal Pos o snd) lits in
    8.40 +  let val (pos, neg) = List.partition (curry (op =) Pos o snd) lits in
    8.41      print_g ("*** Solution:\n" ^
    8.42               "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
    8.43               "-: " ^ commas (map (string_for_var o fst) neg))
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Dec 14 12:14:12 2009 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Dec 14 12:30:26 2009 +0100
     9.3 @@ -716,16 +716,16 @@
     9.4               else if is_rep_fun thy x then
     9.5                 Func oo best_non_opt_symmetric_reps_for_fun_type
     9.6               else if all_precise orelse is_skolem_name v
     9.7 -                     orelse original_name s
     9.8 -                            mem [@{const_name undefined_fast_The},
     9.9 -                                 @{const_name undefined_fast_Eps},
    9.10 -                                 @{const_name bisim},
    9.11 -                                 @{const_name bisim_iterator_max}] then
    9.12 +                     orelse member (op =) [@{const_name undefined_fast_The},
    9.13 +                                           @{const_name undefined_fast_Eps},
    9.14 +                                           @{const_name bisim},
    9.15 +                                           @{const_name bisim_iterator_max}]
    9.16 +                                          (original_name s) then
    9.17                 best_non_opt_set_rep_for_type
    9.18 -             else if original_name s
    9.19 -                     mem [@{const_name set}, @{const_name distinct},
    9.20 -                          @{const_name ord_class.less},
    9.21 -                          @{const_name ord_class.less_eq}] then
    9.22 +             else if member (op =) [@{const_name set}, @{const_name distinct},
    9.23 +                                    @{const_name ord_class.less},
    9.24 +                                    @{const_name ord_class.less_eq}]
    9.25 +                                   (original_name s) then
    9.26                 best_set_rep_for_type
    9.27               else
    9.28                 best_opt_set_rep_for_type) scope T
    9.29 @@ -934,20 +934,21 @@
    9.30              Cst (NormFrac, T, Func (R1, Func (R1, Opt (Struct [R1, R1]))))
    9.31            end
    9.32          | Cst (cst, T, _) =>
    9.33 -          if cst mem [Unknown, Unrep] then
    9.34 +          if cst = Unknown orelse cst = Unrep then
    9.35              case (is_boolean_type T, polar) of
    9.36                (true, Pos) => Cst (False, T, Formula Pos)
    9.37              | (true, Neg) => Cst (True, T, Formula Neg)
    9.38              | _ => Cst (cst, T, best_opt_set_rep_for_type scope T)
    9.39 -          else if cst mem [Add, Subtract, Multiply, Divide, Modulo, Gcd,
    9.40 -                           Lcm] then
    9.41 +          else if member (op =) [Add, Subtract, Multiply, Divide, Modulo, Gcd,
    9.42 +                                 Lcm] cst then
    9.43              let
    9.44                val T1 = domain_type T
    9.45                val R1 = Atom (spec_of_type scope T1)
    9.46                val total =
    9.47 -                T1 = nat_T andalso cst mem [Subtract, Divide, Modulo, Gcd]
    9.48 +                T1 = nat_T andalso (cst = Subtract orelse cst = Divide
    9.49 +                                    orelse cst = Modulo orelse cst = Gcd)
    9.50              in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
    9.51 -          else if cst mem [NatToInt, IntToNat] then
    9.52 +          else if cst = NatToInt orelse cst = IntToNat then
    9.53              let
    9.54                val (nat_card, nat_j0) = spec_of_type scope nat_T
    9.55                val (int_card, int_j0) = spec_of_type scope int_T
    9.56 @@ -1113,7 +1114,7 @@
    9.57               in s_op2 Lambda T R u1' u2' end
    9.58             | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
    9.59          | Op2 (oper, T, _, u1, u2) =>
    9.60 -          if oper mem [All, Exist] then
    9.61 +          if oper = All orelse oper = Exist then
    9.62              let
    9.63                val table' = fold (choose_rep_for_bound_var scope) (untuple I u1)
    9.64                                  table
    9.65 @@ -1140,7 +1141,7 @@
    9.66                      end
    9.67                  end
    9.68              end
    9.69 -          else if oper mem [Or, And] then
    9.70 +          else if oper = Or orelse oper = And then
    9.71              let
    9.72                val u1' = gsub def polar u1
    9.73                val u2' = gsub def polar u2
    9.74 @@ -1159,7 +1160,7 @@
    9.75                   raise SAME ())
    9.76                handle SAME () => s_op2 oper T (Formula polar) u1' u2'
    9.77              end
    9.78 -          else if oper mem [The, Eps] then
    9.79 +          else if oper = The orelse oper = Eps then
    9.80              let
    9.81                val u1' = sub u1
    9.82                val opt1 = is_opt_rep (rep_of u1')
    9.83 @@ -1210,7 +1211,7 @@
    9.84            let
    9.85              val Rs = map (best_one_rep_for_type scope o type_of) us
    9.86              val us = map sub us
    9.87 -            val R = if forall (equal Unit) Rs then Unit else Struct Rs
    9.88 +            val R = if forall (curry (op =) Unit) Rs then Unit else Struct Rs
    9.89              val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R
    9.90            in s_tuple T R' us end
    9.91          | Construct (us', T, _, us) =>
    9.92 @@ -1331,7 +1332,7 @@
    9.93      Cst _ => u
    9.94    | Op1 (oper, T, R, u1) => Op1 (oper, T, R, rename_vars_in_nut pool table u1)
    9.95    | Op2 (oper, T, R, u1, u2) =>
    9.96 -    if oper mem [All, Exist, Lambda] then
    9.97 +    if oper = All orelse oper = Exist orelse oper = Lambda then
    9.98        let
    9.99          val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1)
   9.100                                      ([], pool, table)
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Dec 14 12:14:12 2009 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Dec 14 12:30:26 2009 +0100
    10.3 @@ -85,12 +85,12 @@
    10.4  
    10.5  (* dtype_spec list -> typ -> dtype_spec option *)
    10.6  fun datatype_spec (dtypes : dtype_spec list) T =
    10.7 -  List.find (equal T o #typ) dtypes
    10.8 +  List.find (curry (op =) T o #typ) dtypes
    10.9  
   10.10  (* dtype_spec list -> styp -> constr_spec *)
   10.11  fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
   10.12    | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
   10.13 -    case List.find (equal (s, body_type T) o (apsnd body_type o #const))
   10.14 +    case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
   10.15                     constrs of
   10.16        SOME c => c
   10.17      | NONE => constr_spec dtypes x
   10.18 @@ -125,7 +125,7 @@
   10.19                                  bisim_depth, datatypes, ...} : scope) =
   10.20    let
   10.21      val (iter_asgns, card_asgns) =
   10.22 -      card_assigns |> filter_out (equal @{typ bisim_iterator} o fst)
   10.23 +      card_assigns |> filter_out (curry (op =) @{typ bisim_iterator} o fst)
   10.24                     |> List.partition (is_fp_iterator_type o fst)
   10.25      val (unimportant_card_asgns, important_card_asgns) =
   10.26        card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
   10.27 @@ -262,14 +262,14 @@
   10.28      (* int list -> int *)
   10.29      fun cost_with_monos [] = 0
   10.30        | cost_with_monos (k :: ks) =
   10.31 -        if k < sync_threshold andalso forall (equal k) ks then
   10.32 +        if k < sync_threshold andalso forall (curry (op =) k) ks then
   10.33            k - sync_threshold
   10.34          else
   10.35            k * (k + 1) div 2 + Integer.sum ks
   10.36      fun cost_without_monos [] = 0
   10.37        | cost_without_monos [k] = k
   10.38        | cost_without_monos (_ :: k :: ks) =
   10.39 -        if k < sync_threshold andalso forall (equal k) ks then
   10.40 +        if k < sync_threshold andalso forall (curry (op =) k) ks then
   10.41            k - sync_threshold
   10.42          else
   10.43            Integer.sum (k :: ks)
   10.44 @@ -282,7 +282,7 @@
   10.45  
   10.46  (* typ -> bool *)
   10.47  fun is_self_recursive_constr_type T =
   10.48 -  exists (exists_subtype (equal (body_type T))) (binder_types T)
   10.49 +  exists (exists_subtype (curry (op =) (body_type T))) (binder_types T)
   10.50  
   10.51  (* (styp * int) list -> styp -> int *)
   10.52  fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x)
   10.53 @@ -436,12 +436,12 @@
   10.54  fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
   10.55                                          (desc as (card_asgns, _)) (T, card) =
   10.56    let
   10.57 -    val shallow = T mem shallow_dataTs
   10.58 +    val shallow = member (op =) shallow_dataTs T
   10.59      val co = is_codatatype thy T
   10.60      val xs = boxed_datatype_constrs ext_ctxt T
   10.61      val self_recs = map (is_self_recursive_constr_type o snd) xs
   10.62      val (num_self_recs, num_non_self_recs) =
   10.63 -      List.partition (equal true) self_recs |> pairself length
   10.64 +      List.partition (curry (op =) true) self_recs |> pairself length
   10.65      val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0
   10.66                                                         card_asgns T)
   10.67      (* int -> int *)