# HG changeset patch
# User blanchet
# Date 1259943541 -3600
# Node ID a28733ef3a8260816769203a64c1f93db3624083
# Parent  854e12dafd28d99c79cd9517d054b427377869a7
export symbols from Minipick (so I can use them in other programs)

diff -r 854e12dafd28 -r a28733ef3a82 src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Fri Dec 04 17:18:07 2009 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Fri Dec 04 17:19:01 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Nitpick/Tools/minipick.ML
+(*  Title:      HOL/Tools/Nitpick/minipick.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009
 
@@ -7,6 +7,18 @@
 
 signature MINIPICK =
 sig
+  datatype rep = SRep | RRep
+  type styp = Nitpick_Util.styp
+
+  val vars_for_bound_var :
+    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
+  val rel_expr_for_bound_var :
+    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
+  val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
+  val false_atom : Kodkod.rel_expr
+  val true_atom : Kodkod.rel_expr
+  val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
+  val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
   val pick_nits_in_term : Proof.context -> (typ -> int) -> term -> string
 end;
 
@@ -19,7 +31,9 @@
 open Nitpick_Peephole
 open Nitpick_Kodkod
 
-(* theory -> typ -> unit *)
+datatype rep = SRep | RRep
+
+(* Proof.context -> typ -> unit *)
 fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts
   | check_type ctxt (Type ("*", Ts)) = List.app (check_type ctxt) Ts
   | check_type _ @{typ bool} = ()
@@ -28,43 +42,35 @@
   | check_type ctxt T =
     raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
 
-(* (typ -> int) -> typ -> int *)
-fun atom_schema_of_one scope (Type ("fun", [T1, T2])) =
-    replicate_list (scope T1) (atom_schema_of_one scope T2)
-  | atom_schema_of_one scope (Type ("*", [T1, T2])) =
-    atom_schema_of_one scope T1 @ atom_schema_of_one scope T2
-  | atom_schema_of_one scope T = [scope T]
-fun atom_schema_of_set scope (Type ("fun", [T1, @{typ bool}])) =
-    atom_schema_of_one scope T1
-  | atom_schema_of_set scope (Type ("fun", [T1, T2])) =
-    atom_schema_of_one scope T1 @ atom_schema_of_set scope T2
-  | atom_schema_of_set scope T = atom_schema_of_one scope T
-val arity_of_one = length oo atom_schema_of_one
-val arity_of_set = length oo atom_schema_of_set
+(* rep -> (typ -> int) -> typ -> int list *)
+fun atom_schema_of SRep card (Type ("fun", [T1, T2])) =
+    replicate_list (card T1) (atom_schema_of SRep card T2)
+  | atom_schema_of RRep card (Type ("fun", [T1, @{typ bool}])) =
+    atom_schema_of SRep card T1
+  | atom_schema_of RRep card (Type ("fun", [T1, T2])) =
+    atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
+  | atom_schema_of _ card (Type ("*", Ts)) = maps (atom_schema_of SRep card) Ts
+  | atom_schema_of _ card T = [card T]
+(* rep -> (typ -> int) -> typ -> int *)
+val arity_of = length ooo atom_schema_of
 
 (* (typ -> int) -> typ list -> int -> int *)
 fun index_for_bound_var _ [_] 0 = 0
-  | index_for_bound_var scope (_ :: Ts) 0 =
-    index_for_bound_var scope Ts 0 + arity_of_one scope (hd Ts)
-  | index_for_bound_var scope Ts n = index_for_bound_var scope (tl Ts) (n - 1)
-(* (typ -> int) -> typ list -> int -> rel_expr list *)
-fun one_vars_for_bound_var scope Ts j =
-  map (curry Var 1) (index_seq (index_for_bound_var scope Ts j)
-                               (arity_of_one scope (nth Ts j)))
-fun set_vars_for_bound_var scope Ts j =
-  map (curry Var 1) (index_seq (index_for_bound_var scope Ts j)
-                               (arity_of_set scope (nth Ts j)))
-(* (typ -> int) -> typ list -> typ -> decl list *)
-fun decls_for_one scope Ts T =
+  | index_for_bound_var card (_ :: Ts) 0 =
+    index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts)
+  | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
+(* (typ -> int) -> rep -> typ list -> int -> rel_expr list *)
+fun vars_for_bound_var card R Ts j =
+  map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
+                               (arity_of R card (nth Ts j)))
+(* (typ -> int) -> rep -> typ list -> int -> rel_expr *)
+val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
+(* rep -> (typ -> int) -> typ list -> typ -> decl list *)
+fun decls_for R card Ts T =
   map2 (curry DeclOne o pair 1)
-       (index_seq (index_for_bound_var scope (T :: Ts) 0)
-                  (arity_of_one scope (nth (T :: Ts) 0)))
-       (map (AtomSeq o rpair 0) (atom_schema_of_one scope T))
-fun decls_for_set scope Ts T =
-  map2 (curry DeclOne o pair 1)
-       (index_seq (index_for_bound_var scope (T :: Ts) 0)
-                  (arity_of_set scope (nth (T :: Ts) 0)))
-       (map (AtomSeq o rpair 0) (atom_schema_of_set scope T))
+       (index_seq (index_for_bound_var card (T :: Ts) 0)
+                  (arity_of R card (nth (T :: Ts) 0)))
+       (map (AtomSeq o rpair 0) (atom_schema_of R card T))
 
 (* int list -> rel_expr *)
 val atom_product = foldl1 Product o map Atom
@@ -78,148 +84,145 @@
 fun atom_from_formula f = RelIf (f, true_atom, false_atom)
 
 (* Proof.context -> (typ -> int) -> styp list -> term -> formula *)
-fun kodkod_formula_for_term ctxt scope frees =
+fun kodkod_formula_for_term ctxt card frees =
   let
-    (* typ list -> int -> rel_expr *)
-    val one_from_bound_var = foldl1 Product oo one_vars_for_bound_var scope
-    val set_from_bound_var = foldl1 Product oo set_vars_for_bound_var scope
     (* typ -> rel_expr -> rel_expr *)
-    fun set_from_one (T as Type ("fun", [T1, @{typ bool}])) r =
+    fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
         let
-          val jss = atom_schema_of_one scope T1 |> map (rpair 0)
+          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
                     |> all_combinations
         in
           map2 (fn i => fn js =>
-                   RelIf (RelEq (Project (r, [Num i]), true_atom),
+                   RelIf (formula_from_atom (Project (r, [Num i])),
                           atom_product js, empty_n_ary_rel (length js)))
                (index_seq 0 (length jss)) jss
           |> foldl1 Union
         end
-      | set_from_one (Type ("fun", [T1, T2])) r =
+      | R_rep_from_S_rep (Type ("fun", [T1, T2])) r =
         let
-          val jss = atom_schema_of_one scope T1 |> map (rpair 0)
+          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
                     |> all_combinations
-          val arity2 = arity_of_one scope T2
+          val arity2 = arity_of SRep card T2
         in
           map2 (fn i => fn js =>
                    Product (atom_product js,
                             Project (r, num_seq (i * arity2) arity2)
-                            |> set_from_one T2))
+                            |> R_rep_from_S_rep T2))
                (index_seq 0 (length jss)) jss
           |> foldl1 Union
         end
-      | set_from_one _ r = r
+      | R_rep_from_S_rep _ r = r
     (* typ list -> typ -> rel_expr -> rel_expr *)
-    fun one_from_set Ts (T as Type ("fun", _)) r =
-        Comprehension (decls_for_one scope Ts T,
-                       RelEq (set_from_one T (one_from_bound_var (T :: Ts) 0),
-                              r))
-      | one_from_set _ _ r = r
+    fun S_rep_from_R_rep Ts (T as Type ("fun", _)) r =
+        Comprehension (decls_for SRep card Ts T,
+            RelEq (R_rep_from_S_rep T
+                       (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
+      | S_rep_from_R_rep _ _ r = r
     (* typ list -> term -> formula *)
-    fun to_f Ts t =
+    fun to_F Ts t =
       (case t of
-         @{const Not} $ t1 => Not (to_f Ts t1)
+         @{const Not} $ t1 => Not (to_F Ts t1)
        | @{const False} => False
        | @{const True} => True
        | Const (@{const_name All}, _) $ Abs (s, T, t') =>
-         All (decls_for_one scope Ts T, to_f (T :: Ts) t')
+         All (decls_for SRep card Ts T, to_F (T :: Ts) t')
        | (t0 as Const (@{const_name All}, _)) $ t1 =>
-         to_f Ts (t0 $ eta_expand Ts t1 1)
+         to_F Ts (t0 $ eta_expand Ts t1 1)
        | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
-         Exist (decls_for_one scope Ts T, to_f (T :: Ts) t')
+         Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
        | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
-         to_f Ts (t0 $ eta_expand Ts t1 1)
+         to_F Ts (t0 $ eta_expand Ts t1 1)
        | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
-         RelEq (to_set Ts t1, to_set Ts t2)
+         RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
        | Const (@{const_name ord_class.less_eq},
                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
-         Subset (to_set Ts t1, to_set Ts t2)
-       | @{const "op &"} $ t1 $ t2 => And (to_f Ts t1, to_f Ts t2)
-       | @{const "op |"} $ t1 $ t2 => Or (to_f Ts t1, to_f Ts t2)
-       | @{const "op -->"} $ t1 $ t2 => Implies (to_f Ts t1, to_f Ts t2)
-       | t1 $ t2 => Subset (to_one Ts t2, to_set Ts t1)
+         Subset (to_R_rep Ts t1, to_R_rep Ts t2)
+       | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
+       | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
+       | @{const "op -->"} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
+       | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
        | Free _ => raise SAME ()
        | Term.Var _ => raise SAME ()
        | Bound _ => raise SAME ()
        | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
-       | _ => raise TERM ("to_f", [t]))
-      handle SAME () => formula_from_atom (to_set Ts t)
+       | _ => raise TERM ("Minipick.kodkod_formula_for_term.to_F", [t]))
+      handle SAME () => formula_from_atom (to_R_rep Ts t)
     (* typ list -> term -> rel_expr *)
-    and to_one Ts t =
+    and to_S_rep Ts t =
         case t of
           Const (@{const_name Pair}, _) $ t1 $ t2 =>
-          Product (to_one Ts t1, to_one Ts t2)
-        | Const (@{const_name Pair}, _) $ _ => to_one Ts (eta_expand Ts t 1)
-        | Const (@{const_name Pair}, _) => to_one Ts (eta_expand Ts t 2)
+          Product (to_S_rep Ts t1, to_S_rep Ts t2)
+        | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
+        | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
         | Const (@{const_name fst}, _) $ t1 =>
-          let val fst_arity = arity_of_one scope (fastype_of1 (Ts, t)) in
-            Project (to_one Ts t1, num_seq 0 fst_arity)
+          let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in
+            Project (to_S_rep Ts t1, num_seq 0 fst_arity)
           end
-        | Const (@{const_name fst}, _) => to_one Ts (eta_expand Ts t 1)
+        | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
         | Const (@{const_name snd}, _) $ t1 =>
           let
-            val pair_arity = arity_of_one scope (fastype_of1 (Ts, t1))
-            val snd_arity = arity_of_one scope (fastype_of1 (Ts, t))
+            val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))
+            val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))
             val fst_arity = pair_arity - snd_arity
-          in Project (to_one Ts t1, num_seq fst_arity snd_arity) end
-        | Const (@{const_name snd}, _) => to_one Ts (eta_expand Ts t 1)
-        | Bound j => one_from_bound_var Ts j
-        | _ => one_from_set Ts (fastype_of1 (Ts, t)) (to_set Ts t)
+          in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
+        | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
+        | Bound j => rel_expr_for_bound_var card SRep Ts j
+        | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
     (* term -> rel_expr *)
-    and to_set Ts t =
+    and to_R_rep Ts t =
       (case t of
-         @{const Not} => to_set Ts (eta_expand Ts t 1)
-       | Const (@{const_name All}, _) => to_set Ts (eta_expand Ts t 1)
-       | Const (@{const_name Ex}, _) => to_set Ts (eta_expand Ts t 1)
-       | Const (@{const_name "op ="}, _) $ _ => to_set Ts (eta_expand Ts t 1)
-       | Const (@{const_name "op ="}, _) => to_set Ts (eta_expand Ts t 2)
+         @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
+       | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
+       | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
+       | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name ord_class.less_eq},
                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
-         to_set Ts (eta_expand Ts t 1)
+         to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name ord_class.less_eq}, _) =>
-         to_set Ts (eta_expand Ts t 2)
-       | @{const "op &"} $ _ => to_set Ts (eta_expand Ts t 1)
-       | @{const "op &"} => to_set Ts (eta_expand Ts t 2)
-       | @{const "op |"} $ _ => to_set Ts (eta_expand Ts t 1)
-       | @{const "op |"} => to_set Ts (eta_expand Ts t 2)
-       | @{const "op -->"} $ _ => to_set Ts (eta_expand Ts t 1)
-       | @{const "op -->"} => to_set Ts (eta_expand Ts t 2)
+         to_R_rep Ts (eta_expand Ts t 2)
+       | @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
+       | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
+       | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name bot_class.bot},
                 T as Type ("fun", [_, @{typ bool}])) =>
-         empty_n_ary_rel (arity_of_set scope T)
+         empty_n_ary_rel (arity_of RRep card T)
        | Const (@{const_name insert}, _) $ t1 $ t2 =>
-         Union (to_one Ts t1, to_set Ts t2)
-       | Const (@{const_name insert}, _) $ _ => to_set Ts (eta_expand Ts t 1)
-       | Const (@{const_name insert}, _) => to_set Ts (eta_expand Ts t 2)
+         Union (to_S_rep Ts t1, to_R_rep Ts t2)
+       | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name trancl}, _) $ t1 =>
-         if arity_of_set scope (fastype_of1 (Ts, t1)) = 2 then
-           Closure (to_set Ts t1)
+         if arity_of RRep card (fastype_of1 (Ts, t1)) = 2 then
+           Closure (to_R_rep Ts t1)
          else
            raise NOT_SUPPORTED "transitive closure for function or pair type"
-       | Const (@{const_name trancl}, _) => to_set Ts (eta_expand Ts t 1)
+       | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name lower_semilattice_class.inf},
                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
-         Intersect (to_set Ts t1, to_set Ts t2)
+         Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
        | Const (@{const_name lower_semilattice_class.inf}, _) $ _ =>
-         to_set Ts (eta_expand Ts t 1)
+         to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name lower_semilattice_class.inf}, _) =>
-         to_set Ts (eta_expand Ts t 2)
+         to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name upper_semilattice_class.sup},
                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
-         Union (to_set Ts t1, to_set Ts t2)
+         Union (to_R_rep Ts t1, to_R_rep Ts t2)
        | Const (@{const_name upper_semilattice_class.sup}, _) $ _ =>
-         to_set Ts (eta_expand Ts t 1)
+         to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name upper_semilattice_class.sup}, _) =>
-         to_set Ts (eta_expand Ts t 2)
+         to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name minus_class.minus},
                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
-         Difference (to_set Ts t1, to_set Ts t2)
+         Difference (to_R_rep Ts t1, to_R_rep Ts t2)
        | Const (@{const_name minus_class.minus},
                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
-         to_set Ts (eta_expand Ts t 1)
+         to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name minus_class.minus},
                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) =>
-         to_set Ts (eta_expand Ts t 2)
+         to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
        | Const (@{const_name Pair}, _) $ _ => raise SAME ()
        | Const (@{const_name Pair}, _) => raise SAME ()
@@ -227,90 +230,90 @@
        | Const (@{const_name fst}, _) => raise SAME ()
        | Const (@{const_name snd}, _) $ _ => raise SAME ()
        | Const (@{const_name snd}, _) => raise SAME ()
-       | Const (_, @{typ bool}) => atom_from_formula (to_f Ts t)
+       | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
        | Free (x as (_, T)) =>
-         Rel (arity_of_set scope T, find_index (equal x) frees)
+         Rel (arity_of RRep card T, find_index (equal x) frees)
        | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
        | Bound j => raise SAME ()
        | Abs (_, T, t') =>
          (case fastype_of1 (T :: Ts, t') of
-            @{typ bool} => Comprehension (decls_for_one scope Ts T,
-                                          to_f (T :: Ts) t')
-          | T' => Comprehension (decls_for_one scope Ts T @
-                                 decls_for_set scope (T :: Ts) T',
-                                 Subset (set_from_bound_var (T' :: T :: Ts) 0,
-                                         to_set (T :: Ts) t')))
+            @{typ bool} => Comprehension (decls_for SRep card Ts T,
+                                          to_F (T :: Ts) t')
+          | T' => Comprehension (decls_for SRep card Ts T @
+                                 decls_for RRep card (T :: Ts) T',
+                                 Subset (rel_expr_for_bound_var card RRep
+                                                              (T' :: T :: Ts) 0,
+                                         to_R_rep (T :: Ts) t')))
        | t1 $ t2 =>
          (case fastype_of1 (Ts, t) of
-            @{typ bool} => atom_from_formula (to_f Ts t)
+            @{typ bool} => atom_from_formula (to_F Ts t)
           | T =>
             let val T2 = fastype_of1 (Ts, t2) in
-              case arity_of_one scope T2 of
-                1 => Join (to_one Ts t2, to_set Ts t1)
+              case arity_of SRep card T2 of
+                1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
               | n =>
                 let
-                  val arity2 = arity_of_one scope T2
-                  val res_arity = arity_of_set scope T
+                  val arity2 = arity_of SRep card T2
+                  val res_arity = arity_of RRep card T
                 in
                   Project (Intersect
-                      (Product (to_one Ts t2,
-                                atom_schema_of_set scope T
+                      (Product (to_S_rep Ts t2,
+                                atom_schema_of RRep card T
                                 |> map (AtomSeq o rpair 0) |> foldl1 Product),
-                       to_set Ts t1),
+                       to_R_rep Ts t1),
                       num_seq arity2 res_arity)
                 end
             end)
        | _ => raise NOT_SUPPORTED ("term " ^
                                    quote (Syntax.string_of_term ctxt t)))
-      handle SAME () => set_from_one (fastype_of1 (Ts, t)) (to_one Ts t)
-  in to_f [] end
+      handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
+  in to_F [] end
 
 (* (typ -> int) -> int -> styp -> bound *)
-fun bound_for_free scope i (s, T) =
-  let val js = atom_schema_of_set scope T in
+fun bound_for_free card i (s, T) =
+  let val js = atom_schema_of RRep card T in
     ([((length js, i), s)],
-     [TupleSet [], atom_schema_of_set scope T |> map (rpair 0)
+     [TupleSet [], atom_schema_of RRep card T |> map (rpair 0)
                    |> tuple_set_from_atom_schema])
   end
 
 (* (typ -> int) -> typ list -> typ -> rel_expr -> formula *)
-fun declarative_axiom_for_rel_expr scope Ts (Type ("fun", [T1, T2])) r =
+fun declarative_axiom_for_rel_expr card Ts (Type ("fun", [T1, T2])) r =
     if body_type T2 = bool_T then
       True
     else
-      All (decls_for_one scope Ts T1,
-           declarative_axiom_for_rel_expr scope (T1 :: Ts) T2
-               (List.foldl Join r (one_vars_for_bound_var scope (T1 :: Ts) 0)))
+      All (decls_for SRep card Ts T1,
+           declarative_axiom_for_rel_expr card (T1 :: Ts) T2
+               (List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0)))
   | declarative_axiom_for_rel_expr _ _ _ r = One r
-
-(* (typ -> int) -> int -> styp -> formula *)
-fun declarative_axiom_for_free scope i (_, T) =
-  declarative_axiom_for_rel_expr scope [] T (Rel (arity_of_set scope T, i))
+(* (typ -> int) -> bool -> int -> styp -> formula *)
+fun declarative_axiom_for_free card i (_, T) =
+  declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
 
 (* Proof.context -> (typ -> int) -> term -> string *)
-fun pick_nits_in_term ctxt raw_scope t =
+fun pick_nits_in_term ctxt raw_card t =
   let
     val thy = ProofContext.theory_of ctxt
+    val {overlord, ...} = Nitpick_Isar.default_params thy []
     (* typ -> int *)
-    fun scope (Type ("fun", [T1, T2])) = reasonable_power (scope T2) (scope T1)
-      | scope (Type ("*", [T1, T2])) = scope T1 * scope T2
-      | scope @{typ bool} = 2
-      | scope T = Int.max (1, raw_scope T)
+    fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1)
+      | card (Type ("*", [T1, T2])) = card T1 * card T2
+      | card @{typ bool} = 2
+      | card T = Int.max (1, raw_card T)
     val neg_t = @{const Not} $ ObjectLogic.atomize_term thy t
     val _ = fold_types (K o check_type ctxt) neg_t ()
     val frees = Term.add_frees neg_t []
-    val bounds = map2 (bound_for_free scope) (index_seq 0 (length frees)) frees
+    val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
     val declarative_axioms =
-      map2 (declarative_axiom_for_free scope) (index_seq 0 (length frees))
-           frees
-    val formula = kodkod_formula_for_term ctxt scope frees neg_t
+      map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
+    val formula = kodkod_formula_for_term ctxt card frees neg_t
                   |> fold_rev (curry And) declarative_axioms
     val univ_card = univ_card 0 0 0 bounds formula
     val problem =
       {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
        bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
   in
-    case solve_any_problem true NONE 0 1 [problem] of
+    case solve_any_problem overlord NONE 0 1 [problem] of
       Normal ([], _) => "none"
     | Normal _ => "genuine"
     | TimedOut _ => "unknown"
@@ -319,4 +322,5 @@
   end
   handle NOT_SUPPORTED details =>
          (warning ("Unsupported case: " ^ details ^ "."); "unknown")
+
 end;