get rid of all "optimizations" regarding "unit" and other cardinality-1 types
authorblanchet
Wed Aug 04 10:39:35 2010 +0200 (2010-08-04)
changeset 38190b02e204b613a
parent 38189 a493dc2179a3
child 38191 deaef70a8c05
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick_hol.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_preproc.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
     1.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Tue Aug 03 21:37:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Aug 04 10:39:35 2010 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  
     1.5  fun check_type ctxt (Type (@{type_name fun}, Ts)) =
     1.6      List.app (check_type ctxt) Ts
     1.7 -  | check_type ctxt (Type (@{type_name Product_Type.prod}, Ts)) =
     1.8 +  | check_type ctxt (Type (@{type_name prod}, Ts)) =
     1.9      List.app (check_type ctxt) Ts
    1.10    | check_type _ @{typ bool} = ()
    1.11    | check_type _ (TFree (_, @{sort "{}"})) = ()
    1.12 @@ -51,7 +51,7 @@
    1.13      atom_schema_of SRep card T1
    1.14    | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
    1.15      atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
    1.16 -  | atom_schema_of _ card (Type (@{type_name Product_Type.prod}, Ts)) =
    1.17 +  | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
    1.18      maps (atom_schema_of SRep card) Ts
    1.19    | atom_schema_of _ card T = [card T]
    1.20  val arity_of = length ooo atom_schema_of
    1.21 @@ -290,7 +290,7 @@
    1.22      val thy = ProofContext.theory_of ctxt
    1.23      fun card (Type (@{type_name fun}, [T1, T2])) =
    1.24          reasonable_power (card T2) (card T1)
    1.25 -      | card (Type (@{type_name Product_Type.prod}, [T1, T2])) = card T1 * card T2
    1.26 +      | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
    1.27        | card @{typ bool} = 2
    1.28        | card T = Int.max (1, raw_card T)
    1.29      val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 21:37:12 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 04 10:39:35 2010 +0200
     2.3 @@ -400,7 +400,6 @@
     2.4     (@{const_name "op -->"}, 2),
     2.5     (@{const_name If}, 3),
     2.6     (@{const_name Let}, 2),
     2.7 -   (@{const_name Unity}, 0),
     2.8     (@{const_name Pair}, 2),
     2.9     (@{const_name fst}, 1),
    2.10     (@{const_name snd}, 1),
    2.11 @@ -456,7 +455,7 @@
    2.12    | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
    2.13      unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
    2.14    | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
    2.15 -    Type (@{type_name Product_Type.prod}, map unarize_unbox_etc_type Ts)
    2.16 +    Type (@{type_name prod}, map unarize_unbox_etc_type Ts)
    2.17    | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
    2.18    | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
    2.19    | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
    2.20 @@ -512,7 +511,7 @@
    2.21    | is_fun_type _ = false
    2.22  fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
    2.23    | is_set_type _ = false
    2.24 -fun is_pair_type (Type (@{type_name Product_Type.prod}, _)) = true
    2.25 +fun is_pair_type (Type (@{type_name prod}, _)) = true
    2.26    | is_pair_type _ = false
    2.27  fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
    2.28    | is_lfp_iterator_type _ = false
    2.29 @@ -549,7 +548,7 @@
    2.30    | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
    2.31  val nth_range_type = snd oo strip_n_binders
    2.32  
    2.33 -fun num_factors_in_type (Type (@{type_name Product_Type.prod}, [T1, T2])) =
    2.34 +fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) =
    2.35      fold (Integer.add o num_factors_in_type) [T1, T2] 0
    2.36    | num_factors_in_type _ = 1
    2.37  fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
    2.38 @@ -560,7 +559,7 @@
    2.39    (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
    2.40  
    2.41  fun mk_flat_tuple _ [t] = t
    2.42 -  | mk_flat_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) (t :: ts) =
    2.43 +  | mk_flat_tuple (Type (@{type_name prod}, [T1, T2])) (t :: ts) =
    2.44      HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
    2.45    | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
    2.46  fun dest_n_tuple 1 t = [t]
    2.47 @@ -598,8 +597,8 @@
    2.48  (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
    2.49     e.g., by adding a field to "Datatype_Aux.info". *)
    2.50  fun is_basic_datatype thy stds s =
    2.51 -  member (op =) [@{type_name Product_Type.prod}, @{type_name bool}, @{type_name unit},
    2.52 -                 @{type_name int}, "Code_Numeral.code_numeral"] s orelse
    2.53 +  member (op =) [@{type_name prod}, @{type_name bool}, @{type_name int},
    2.54 +                 "Code_Numeral.code_numeral"] s orelse
    2.55    (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
    2.56  
    2.57  fun instantiate_type thy T1 T1' T2 =
    2.58 @@ -795,7 +794,7 @@
    2.59      Type (@{type_name fun}, _) =>
    2.60      (boxy = InPair orelse boxy = InFunLHS) andalso
    2.61      not (is_boolean_type (body_type T))
    2.62 -  | Type (@{type_name Product_Type.prod}, Ts) =>
    2.63 +  | Type (@{type_name prod}, Ts) =>
    2.64      boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
    2.65      ((boxy = InExpr orelse boxy = InFunLHS) andalso
    2.66       exists (is_boxing_worth_it hol_ctxt InPair)
    2.67 @@ -815,12 +814,12 @@
    2.68      else
    2.69        box_type hol_ctxt (in_fun_lhs_for boxy) T1
    2.70        --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
    2.71 -  | Type (z as (@{type_name Product_Type.prod}, Ts)) =>
    2.72 +  | Type (z as (@{type_name prod}, Ts)) =>
    2.73      if boxy <> InConstr andalso boxy <> InSel
    2.74         andalso should_box_type hol_ctxt boxy z then
    2.75        Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
    2.76      else
    2.77 -      Type (@{type_name Product_Type.prod},
    2.78 +      Type (@{type_name prod},
    2.79              map (box_type hol_ctxt
    2.80                            (if boxy = InConstr orelse boxy = InSel then boxy
    2.81                             else InPair)) Ts)
    2.82 @@ -982,7 +981,7 @@
    2.83        Const (nth_sel_for_constr x n)
    2.84      else
    2.85        let
    2.86 -        fun aux m (Type (@{type_name Product_Type.prod}, [T1, T2])) =
    2.87 +        fun aux m (Type (@{type_name prod}, [T1, T2])) =
    2.88              let
    2.89                val (m, t1) = aux m T1
    2.90                val (m, t2) = aux m T2
    2.91 @@ -1072,7 +1071,7 @@
    2.92      | (Type (new_s, new_Ts as [new_T1, new_T2]),
    2.93         Type (old_s, old_Ts as [old_T1, old_T2])) =>
    2.94        if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
    2.95 -         old_s = @{type_name pair_box} orelse old_s = @{type_name Product_Type.prod} then
    2.96 +         old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then
    2.97          case constr_expand hol_ctxt old_T t of
    2.98            Const (old_s, _) $ t1 =>
    2.99            if new_s = @{type_name fun} then
   2.100 @@ -1084,7 +1083,7 @@
   2.101                               (Type (@{type_name fun}, old_Ts)) t1]
   2.102          | Const _ $ t1 $ t2 =>
   2.103            construct_value ctxt stds
   2.104 -              (if new_s = @{type_name Product_Type.prod} then @{const_name Pair}
   2.105 +              (if new_s = @{type_name prod} then @{const_name Pair}
   2.106                 else @{const_name PairBox}, new_Ts ---> new_T)
   2.107                (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
   2.108                      [t1, t2])
   2.109 @@ -1095,12 +1094,11 @@
   2.110  
   2.111  fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
   2.112      reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
   2.113 -  | card_of_type assigns (Type (@{type_name Product_Type.prod}, [T1, T2])) =
   2.114 +  | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
   2.115      card_of_type assigns T1 * card_of_type assigns T2
   2.116    | card_of_type _ (Type (@{type_name itself}, _)) = 1
   2.117    | card_of_type _ @{typ prop} = 2
   2.118    | card_of_type _ @{typ bool} = 2
   2.119 -  | card_of_type _ @{typ unit} = 1
   2.120    | card_of_type assigns T =
   2.121      case AList.lookup (op =) assigns T of
   2.122        SOME k => k
   2.123 @@ -1116,7 +1114,7 @@
   2.124        else Int.min (max, reasonable_power k2 k1)
   2.125      end
   2.126    | bounded_card_of_type max default_card assigns
   2.127 -                         (Type (@{type_name Product_Type.prod}, [T1, T2])) =
   2.128 +                         (Type (@{type_name prod}, [T1, T2])) =
   2.129      let
   2.130        val k1 = bounded_card_of_type max default_card assigns T1
   2.131        val k2 = bounded_card_of_type max default_card assigns T2
   2.132 @@ -1146,7 +1144,7 @@
   2.133             else if k1 >= max orelse k2 >= max then max
   2.134             else Int.min (max, reasonable_power k2 k1)
   2.135           end
   2.136 -       | Type (@{type_name Product_Type.prod}, [T1, T2]) =>
   2.137 +       | Type (@{type_name prod}, [T1, T2]) =>
   2.138           let
   2.139             val k1 = aux avoid T1
   2.140             val k2 = aux avoid T2
   2.141 @@ -1158,7 +1156,6 @@
   2.142         | Type (@{type_name itself}, _) => 1
   2.143         | @{typ prop} => 2
   2.144         | @{typ bool} => 2
   2.145 -       | @{typ unit} => 1
   2.146         | Type _ =>
   2.147           (case datatype_constrs hol_ctxt T of
   2.148              [] => if is_integer_type T orelse is_bit_type T then 0
   2.149 @@ -1198,9 +1195,10 @@
   2.150  fun special_bounds ts =
   2.151    fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
   2.152  
   2.153 +(* FIXME: detect "rep_datatype"? *)
   2.154  fun is_funky_typedef_name thy s =
   2.155 -  member (op =) [@{type_name unit}, @{type_name Product_Type.prod}, @{type_name Sum_Type.sum},
   2.156 -                 @{type_name int}] s orelse
   2.157 +  member (op =) [@{type_name unit}, @{type_name prod},
   2.158 +                 @{type_name Sum_Type.sum}, @{type_name int}] s orelse
   2.159    is_frac_type thy (Type (s, []))
   2.160  fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
   2.161    | is_funky_typedef _ _ = false
   2.162 @@ -2088,7 +2086,7 @@
   2.163      val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
   2.164      val set_T = tuple_T --> bool_T
   2.165      val curried_T = tuple_T --> set_T
   2.166 -    val uncurried_T = Type (@{type_name Product_Type.prod}, [tuple_T, tuple_T]) --> bool_T
   2.167 +    val uncurried_T = Type (@{type_name prod}, [tuple_T, tuple_T]) --> bool_T
   2.168      val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
   2.169      val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
   2.170      val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
   2.171 @@ -2215,11 +2213,10 @@
   2.172      fun aux T accum =
   2.173        case T of
   2.174          Type (@{type_name fun}, Ts) => fold aux Ts accum
   2.175 -      | Type (@{type_name Product_Type.prod}, Ts) => fold aux Ts accum
   2.176 +      | Type (@{type_name prod}, Ts) => fold aux Ts accum
   2.177        | Type (@{type_name itself}, [T1]) => aux T1 accum
   2.178        | Type (_, Ts) =>
   2.179 -        if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
   2.180 -                  T then
   2.181 +        if member (op =) (@{typ prop} :: @{typ bool} :: accum) T then
   2.182            accum
   2.183          else
   2.184            T :: accum
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Aug 03 21:37:12 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Aug 04 10:39:35 2010 +0200
     3.3 @@ -492,24 +492,19 @@
     3.4    case old_R of
     3.5      Atom _ => lone_rep_fallback kk (Struct Rs) old_R r
     3.6    | Struct Rs' =>
     3.7 -    let
     3.8 -      val Rs = filter (not_equal Unit) Rs
     3.9 -      val Rs' = filter (not_equal Unit) Rs'
    3.10 -    in
    3.11 -      if Rs' = Rs then
    3.12 -        r
    3.13 -      else if map card_of_rep Rs' = map card_of_rep Rs then
    3.14 -        let
    3.15 -          val old_arities = map arity_of_rep Rs'
    3.16 -          val old_offsets = offset_list old_arities
    3.17 -          val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities
    3.18 -        in
    3.19 -          fold1 (#kk_product kk)
    3.20 -                (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
    3.21 -        end
    3.22 -      else
    3.23 -        lone_rep_fallback kk (Struct Rs) old_R r
    3.24 -    end
    3.25 +    if Rs' = Rs then
    3.26 +      r
    3.27 +    else if map card_of_rep Rs' = map card_of_rep Rs then
    3.28 +      let
    3.29 +        val old_arities = map arity_of_rep Rs'
    3.30 +        val old_offsets = offset_list old_arities
    3.31 +        val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities
    3.32 +      in
    3.33 +        fold1 (#kk_product kk)
    3.34 +              (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
    3.35 +      end
    3.36 +    else
    3.37 +      lone_rep_fallback kk (Struct Rs) old_R r
    3.38    | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
    3.39  and vect_from_rel_expr kk k R old_R r =
    3.40    case old_R of
    3.41 @@ -525,7 +520,6 @@
    3.42                   (all_singletons_for_rep R1))
    3.43      else
    3.44        raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
    3.45 -  | Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r
    3.46    | Func (R1, R2) =>
    3.47      fold1 (#kk_product kk)
    3.48            (map (fn arg_r =>
    3.49 @@ -541,20 +535,6 @@
    3.50        func_from_no_opt_rel_expr kk R1 R2 (Vect (dom_card, R2'))
    3.51                                  (vect_from_rel_expr kk dom_card R2' (Atom x) r)
    3.52      end
    3.53 -  | func_from_no_opt_rel_expr kk Unit R2 old_R r =
    3.54 -    (case old_R of
    3.55 -       Vect (_, R') => rel_expr_from_rel_expr kk R2 R' r
    3.56 -     | Func (Unit, R2') => rel_expr_from_rel_expr kk R2 R2' r
    3.57 -     | Func (Atom (1, _), Formula Neut) =>
    3.58 -       (case unopt_rep R2 of
    3.59 -          Atom (2, j0) => atom_from_formula kk j0 (#kk_some kk r)
    3.60 -        | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
    3.61 -                          [old_R, Func (Unit, R2)]))
    3.62 -     | Func (R1', R2') =>
    3.63 -       rel_expr_from_rel_expr kk R2 R2' (#kk_project_seq kk r (arity_of_rep R1')
    3.64 -                              (arity_of_rep R2'))
    3.65 -     | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
    3.66 -                       [old_R, Func (Unit, R2)]))
    3.67    | func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r =
    3.68      (case old_R of
    3.69         Vect (k, Atom (2, j0)) =>
    3.70 @@ -578,9 +558,6 @@
    3.71           in
    3.72             #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)
    3.73           end
    3.74 -     | Func (Unit, (Atom (2, j0))) =>
    3.75 -       #kk_rel_if kk (#kk_rel_eq kk r (KK.Atom (j0 + 1)))
    3.76 -                  (full_rel_for_rep R1) (empty_rel_for_rep R1)
    3.77       | Func (R1', Atom (2, j0)) =>
    3.78         func_from_no_opt_rel_expr kk R1 (Formula Neut)
    3.79             (Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1)))
    3.80 @@ -615,11 +592,6 @@
    3.81             end
    3.82           | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
    3.83                             [old_R, Func (R1, R2)]))
    3.84 -    | Func (Unit, R2') =>
    3.85 -      let val j0 = some_j0 in
    3.86 -        func_from_no_opt_rel_expr kk R1 R2 (Func (Atom (1, j0), R2'))
    3.87 -                                  (#kk_product kk (KK.Atom j0) r)
    3.88 -      end
    3.89      | Func (R1', R2') =>
    3.90        if R1 = R1' andalso R2 = R2' then
    3.91          r
    3.92 @@ -1099,9 +1071,7 @@
    3.93               val R2 = rep_of u2
    3.94               val (dom_R, ran_R) =
    3.95                 case min_rep R1 R2 of
    3.96 -                 Func (Unit, R') =>
    3.97 -                 (Atom (1, offset_of_type ofs dom_T), R')
    3.98 -               | Func Rp => Rp
    3.99 +                 Func Rp => Rp
   3.100                 | R => (Atom (card_of_domain_from_rep 2 R,
   3.101                               offset_of_type ofs dom_T),
   3.102                         if is_opt_rep R then Opt bool_atom_R else Formula Neut)
   3.103 @@ -1126,8 +1096,7 @@
   3.104             end
   3.105           | Op2 (DefEq, _, _, u1, u2) =>
   3.106             (case min_rep (rep_of u1) (rep_of u2) of
   3.107 -              Unit => KK.True
   3.108 -            | Formula polar =>
   3.109 +              Formula polar =>
   3.110                kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
   3.111              | min_R =>
   3.112                let
   3.113 @@ -1145,8 +1114,7 @@
   3.114                end)
   3.115           | Op2 (Eq, _, _, u1, u2) =>
   3.116             (case min_rep (rep_of u1) (rep_of u2) of
   3.117 -              Unit => KK.True
   3.118 -            | Formula polar =>
   3.119 +              Formula polar =>
   3.120                kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
   3.121              | min_R =>
   3.122                if is_opt_rep min_R then
   3.123 @@ -1426,11 +1394,10 @@
   3.124              rel_expr_from_rel_expr kk R R' (kk_closure (to_rep R' u1))
   3.125            end
   3.126        | Op1 (SingletonSet, _, Func (R1, Opt _), Cst (Unrep, _, _)) =>
   3.127 -        (if R1 = Unit then I else kk_product (full_rel_for_rep R1)) false_atom
   3.128 +        kk_product (full_rel_for_rep R1) false_atom
   3.129        | Op1 (SingletonSet, _, R, u1) =>
   3.130          (case R of
   3.131             Func (R1, Formula Neut) => to_rep R1 u1
   3.132 -         | Func (Unit, Opt R) => to_guard [u1] R true_atom
   3.133           | Func (R1, Opt _) =>
   3.134             single_rel_rel_let kk
   3.135                 (fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)
   3.136 @@ -1676,10 +1643,8 @@
   3.137             Struct Rs => to_product Rs us
   3.138           | Vect (k, R) => to_product (replicate k R) us
   3.139           | Atom (1, j0) =>
   3.140 -           (case filter (not_equal Unit o rep_of) us of
   3.141 -              [] => KK.Atom j0
   3.142 -            | us' => kk_rel_if (kk_some (fold1 kk_product (map to_r us')))
   3.143 -                               (KK.Atom j0) KK.None)
   3.144 +           kk_rel_if (kk_some (fold1 kk_product (map to_r us)))
   3.145 +                     (KK.Atom j0) KK.None
   3.146           | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
   3.147        | Construct ([u'], _, _, []) => to_r u'
   3.148        | Construct (discr_u :: sel_us, _, _, arg_us) =>
   3.149 @@ -1715,21 +1680,10 @@
   3.150      and to_atom (x as (k, j0)) u =
   3.151        case rep_of u of
   3.152          Formula _ => atom_from_formula kk j0 (to_f u)
   3.153 -      | Unit => if k = 1 then KK.Atom j0
   3.154 -                else raise NUT ("Nitpick_Kodkod.to_atom", [u])
   3.155        | R => atom_from_rel_expr kk x R (to_r u)
   3.156 -    and to_struct Rs u =
   3.157 -      case rep_of u of
   3.158 -        Unit => full_rel_for_rep (Struct Rs)
   3.159 -      | R' => struct_from_rel_expr kk Rs R' (to_r u)
   3.160 -    and to_vect k R u =
   3.161 -      case rep_of u of
   3.162 -        Unit => full_rel_for_rep (Vect (k, R))
   3.163 -      | R' => vect_from_rel_expr kk k R R' (to_r u)
   3.164 -    and to_func R1 R2 u =
   3.165 -      case rep_of u of
   3.166 -        Unit => full_rel_for_rep (Func (R1, R2))
   3.167 -      | R' => rel_expr_to_func kk R1 R2 R' (to_r u)
   3.168 +    and to_struct Rs u = struct_from_rel_expr kk Rs (rep_of u) (to_r u)
   3.169 +    and to_vect k R u = vect_from_rel_expr kk k R (rep_of u) (to_r u)
   3.170 +    and to_func R1 R2 u = rel_expr_to_func kk R1 R2 (rep_of u) (to_r u)
   3.171      and to_opt R u =
   3.172        let val old_R = rep_of u in
   3.173          if is_opt_rep old_R then
   3.174 @@ -1764,10 +1718,7 @@
   3.175      and to_project new_R old_R r j0 =
   3.176        rel_expr_from_rel_expr kk new_R old_R
   3.177                               (kk_project_seq r j0 (arity_of_rep old_R))
   3.178 -    and to_product Rs us =
   3.179 -      case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of
   3.180 -        [] => raise REP ("Nitpick_Kodkod.to_product", Rs)
   3.181 -      | rs => fold1 kk_product rs
   3.182 +    and to_product Rs us = fold1 kk_product (map (uncurry to_opt) (Rs ~~ us))
   3.183      and to_nth_pair_sel n res_T res_R u =
   3.184        case u of
   3.185          Tuple (_, _, us) => to_rep res_R (nth us n)
   3.186 @@ -1789,12 +1740,7 @@
   3.187                     end
   3.188                 val nth_R = nth Rs n
   3.189                 val j0 = if n = 0 then 0 else arity_of_rep (hd Rs)
   3.190 -             in
   3.191 -               case arity_of_rep nth_R of
   3.192 -                 0 => to_guard [u] res_R
   3.193 -                               (to_rep res_R (Cst (Unity, res_T, Unit)))
   3.194 -               | _ => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
   3.195 -             end
   3.196 +             in to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0 end
   3.197      and to_set_bool_op connective set_oper u1 u2 =
   3.198        let
   3.199          val min_R = min_rep (rep_of u1) (rep_of u2)
   3.200 @@ -1804,8 +1750,6 @@
   3.201          case min_R of
   3.202            Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2
   3.203          | Func (_, Formula Neut) => set_oper r1 r2
   3.204 -        | Func (Unit, Atom (2, j0)) =>
   3.205 -          connective (formula_from_atom j0 r1) (formula_from_atom j0 r2)
   3.206          | Func (_, Atom _) => set_oper (kk_join r1 true_atom)
   3.207                                         (kk_join r2 true_atom)
   3.208          | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
   3.209 @@ -1843,12 +1787,7 @@
   3.210          raise REP ("Nitpick_Kodkod.to_apply", [R])
   3.211        | to_apply res_R func_u arg_u =
   3.212          case unopt_rep (rep_of func_u) of
   3.213 -          Unit =>
   3.214 -          let val j0 = offset_of_type ofs (type_of func_u) in
   3.215 -            to_guard [arg_u] res_R
   3.216 -                     (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0))
   3.217 -          end
   3.218 -        | Atom (1, j0) =>
   3.219 +          Atom (1, j0) =>
   3.220            to_guard [arg_u] res_R
   3.221                     (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u))
   3.222          | Atom (k, _) =>
   3.223 @@ -1867,9 +1806,6 @@
   3.224          | Func (R, Formula Neut) =>
   3.225            to_guard [arg_u] res_R (rel_expr_from_formula kk res_R
   3.226                                        (kk_subset (to_opt R arg_u) (to_r func_u)))
   3.227 -        | Func (Unit, R2) =>
   3.228 -          to_guard [arg_u] res_R
   3.229 -                   (rel_expr_from_rel_expr kk res_R R2 (to_r func_u))
   3.230          | Func (R1, R2) =>
   3.231            rel_expr_from_rel_expr kk res_R R2
   3.232                (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Aug 03 21:37:12 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Aug 04 10:39:35 2010 +0200
     4.3 @@ -170,7 +170,7 @@
     4.4                  Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
     4.5           $ t1 $ t2) =
     4.6      let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
     4.7 -      Const (@{const_name Pair}, Ts ---> Type (@{type_name Product_Type.prod}, Ts))
     4.8 +      Const (@{const_name Pair}, Ts ---> Type (@{type_name prod}, Ts))
     4.9        $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
    4.10      end
    4.11    | unarize_unbox_etc_term (Const (s, T)) =
    4.12 @@ -185,27 +185,27 @@
    4.13    | unarize_unbox_etc_term (Abs (s, T, t')) =
    4.14      Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
    4.15  
    4.16 -fun factor_out_types (T1 as Type (@{type_name Product_Type.prod}, [T11, T12]))
    4.17 -                     (T2 as Type (@{type_name Product_Type.prod}, [T21, T22])) =
    4.18 +fun factor_out_types (T1 as Type (@{type_name prod}, [T11, T12]))
    4.19 +                     (T2 as Type (@{type_name prod}, [T21, T22])) =
    4.20      let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
    4.21        if n1 = n2 then
    4.22          let
    4.23            val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
    4.24          in
    4.25 -          ((Type (@{type_name Product_Type.prod}, [T11, T11']), opt_T12'),
    4.26 -           (Type (@{type_name Product_Type.prod}, [T21, T21']), opt_T22'))
    4.27 +          ((Type (@{type_name prod}, [T11, T11']), opt_T12'),
    4.28 +           (Type (@{type_name prod}, [T21, T21']), opt_T22'))
    4.29          end
    4.30        else if n1 < n2 then
    4.31          case factor_out_types T1 T21 of
    4.32            (p1, (T21', NONE)) => (p1, (T21', SOME T22))
    4.33          | (p1, (T21', SOME T22')) =>
    4.34 -          (p1, (T21', SOME (Type (@{type_name Product_Type.prod}, [T22', T22]))))
    4.35 +          (p1, (T21', SOME (Type (@{type_name prod}, [T22', T22]))))
    4.36        else
    4.37          swap (factor_out_types T2 T1)
    4.38      end
    4.39 -  | factor_out_types (Type (@{type_name Product_Type.prod}, [T11, T12])) T2 =
    4.40 +  | factor_out_types (Type (@{type_name prod}, [T11, T12])) T2 =
    4.41      ((T11, SOME T12), (T2, NONE))
    4.42 -  | factor_out_types T1 (Type (@{type_name Product_Type.prod}, [T21, T22])) =
    4.43 +  | factor_out_types T1 (Type (@{type_name prod}, [T21, T22])) =
    4.44      ((T1, NONE), (T21, SOME T22))
    4.45    | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
    4.46  
    4.47 @@ -239,7 +239,7 @@
    4.48      val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
    4.49      val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
    4.50    in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
    4.51 -fun pair_up (Type (@{type_name Product_Type.prod}, [T1', T2']))
    4.52 +fun pair_up (Type (@{type_name prod}, [T1', T2']))
    4.53              (t1 as Const (@{const_name Pair},
    4.54                            Type (@{type_name fun},
    4.55                                  [_, Type (@{type_name fun}, [_, T1])]))
    4.56 @@ -287,8 +287,8 @@
    4.57        and do_term (Type (@{type_name fun}, [T1', T2']))
    4.58                    (Type (@{type_name fun}, [T1, T2])) t =
    4.59            do_fun T1' T2' T1 T2 t
    4.60 -        | do_term (T' as Type (@{type_name Product_Type.prod}, Ts' as [T1', T2']))
    4.61 -                  (Type (@{type_name Product_Type.prod}, [T1, T2]))
    4.62 +        | do_term (T' as Type (@{type_name prod}, Ts' as [T1', T2']))
    4.63 +                  (Type (@{type_name prod}, [T1, T2]))
    4.64                    (Const (@{const_name Pair}, _) $ t1 $ t2) =
    4.65            Const (@{const_name Pair}, Ts' ---> T')
    4.66            $ do_term T1' T1 t1 $ do_term T2' T2 t2
    4.67 @@ -303,7 +303,7 @@
    4.68    | truth_const_sort_key @{const False} = "2"
    4.69    | truth_const_sort_key _ = "1"
    4.70  
    4.71 -fun mk_tuple (Type (@{type_name Product_Type.prod}, [T1, T2])) ts =
    4.72 +fun mk_tuple (Type (@{type_name prod}, [T1, T2])) ts =
    4.73      HOLogic.mk_prod (mk_tuple T1 ts,
    4.74          mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
    4.75    | mk_tuple _ (t :: _) = t
    4.76 @@ -463,7 +463,7 @@
    4.77                              signed_string_of_int j ^ " for " ^
    4.78                              string_for_rep (Vect (k1, Atom (k2, 0))))
    4.79          end
    4.80 -      | term_for_atom seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _ j k =
    4.81 +      | term_for_atom seen (Type (@{type_name prod}, [T1, T2])) _ j k =
    4.82          let
    4.83            val k1 = card_of_type card_assigns T1
    4.84            val k2 = k div k1
    4.85 @@ -476,7 +476,6 @@
    4.86          HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
    4.87        | term_for_atom _ @{typ bool} _ j _ =
    4.88          if j = 0 then @{const False} else @{const True}
    4.89 -      | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
    4.90        | term_for_atom seen T _ j k =
    4.91          if T = nat_T andalso is_standard_datatype thy stds nat_T then
    4.92            HOLogic.mk_number nat_T j
    4.93 @@ -588,11 +587,10 @@
    4.94                 (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
    4.95                 (map (term_for_rep true seen T2 T2 R o single)
    4.96                      (batch_list (arity_of_rep R) js))
    4.97 -    and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1
    4.98 -      | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
    4.99 +    and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
   4.100          if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
   4.101          else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
   4.102 -      | term_for_rep _ seen (Type (@{type_name Product_Type.prod}, [T1, T2])) _
   4.103 +      | term_for_rep _ seen (Type (@{type_name prod}, [T1, T2])) _
   4.104                       (Struct [R1, R2]) [js] =
   4.105          let
   4.106            val arity1 = arity_of_rep R1
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Aug 03 21:37:12 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Aug 04 10:39:35 2010 +0200
     5.3 @@ -254,7 +254,7 @@
     5.4        else case T of
     5.5          Type (@{type_name fun}, [T1, T2]) =>
     5.6          MFun (fresh_mfun_for_fun_type mdata false T1 T2)
     5.7 -      | Type (@{type_name Product_Type.prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
     5.8 +      | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
     5.9        | Type (z as (s, _)) =>
    5.10          if could_exist_alpha_sub_mtype ctxt alpha_T T then
    5.11            case AList.lookup (op =) (!datatype_mcache) z of
    5.12 @@ -1043,8 +1043,8 @@
    5.13            | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
    5.14              Type (if should_finitize T a then @{type_name fin_fun}
    5.15                    else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
    5.16 -          | (MPair (M1, M2), Type (@{type_name Product_Type.prod}, Ts)) =>
    5.17 -            Type (@{type_name Product_Type.prod}, map2 type_from_mtype Ts [M1, M2])
    5.18 +          | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
    5.19 +            Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
    5.20            | (MType _, _) => T
    5.21            | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
    5.22                                [M], [T])
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Aug 03 21:37:12 2010 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Aug 04 10:39:35 2010 +0200
     6.3 @@ -14,7 +14,6 @@
     6.4    type rep = Nitpick_Rep.rep
     6.5  
     6.6    datatype cst =
     6.7 -    Unity |
     6.8      False |
     6.9      True |
    6.10      Iden |
    6.11 @@ -132,7 +131,6 @@
    6.12  structure KK = Kodkod
    6.13  
    6.14  datatype cst =
    6.15 -  Unity |
    6.16    False |
    6.17    True |
    6.18    Iden |
    6.19 @@ -202,8 +200,7 @@
    6.20  
    6.21  exception NUT of string * nut list
    6.22  
    6.23 -fun string_for_cst Unity = "Unity"
    6.24 -  | string_for_cst False = "False"
    6.25 +fun string_for_cst False = "False"
    6.26    | string_for_cst True = "True"
    6.27    | string_for_cst Iden = "Iden"
    6.28    | string_for_cst (Num j) = "Num " ^ signed_string_of_int j
    6.29 @@ -429,7 +426,7 @@
    6.30      let val res_T = snd (HOLogic.dest_prodT T) in
    6.31        (res_T, Const (@{const_name snd}, T --> res_T) $ t)
    6.32      end
    6.33 -fun factorize (z as (Type (@{type_name Product_Type.prod}, _), _)) =
    6.34 +fun factorize (z as (Type (@{type_name prod}, _), _)) =
    6.35      maps factorize [mk_fst z, mk_snd z]
    6.36    | factorize z = [z]
    6.37  
    6.38 @@ -534,7 +531,6 @@
    6.39                 sub t1, sub_abs s T' t2)
    6.40          | (t0 as Const (@{const_name Let}, _), [t1, t2]) =>
    6.41            sub (t0 $ t1 $ eta_expand Ts t2 1)
    6.42 -        | (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
    6.43          | (Const (@{const_name Pair}, T), [t1, t2]) =>
    6.44            Tuple (nth_range_type 2 T, Any, map sub [t1, t2])
    6.45          | (Const (@{const_name fst}, T), [t1]) =>
    6.46 @@ -754,8 +750,6 @@
    6.47    | Construct (_, _, _, us) => forall is_constructive us
    6.48    | _ => false
    6.49  
    6.50 -fun optimize_unit u =
    6.51 -  if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u
    6.52  fun unknown_boolean T R =
    6.53    Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
    6.54         T, R)
    6.55 @@ -768,7 +762,6 @@
    6.56      else
    6.57        raise SAME ())
    6.58     handle SAME () => Op1 (oper, T, R, u1))
    6.59 -  |> optimize_unit
    6.60  fun s_op2 oper T R u1 u2 =
    6.61    ((case oper of
    6.62        All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2
    6.63 @@ -810,7 +803,6 @@
    6.64          raise SAME ()
    6.65      | _ => raise SAME ())
    6.66     handle SAME () => Op2 (oper, T, R, u1, u2))
    6.67 -  |> optimize_unit
    6.68  fun s_op3 oper T R u1 u2 u3 =
    6.69    ((case oper of
    6.70        Let =>
    6.71 @@ -820,13 +812,11 @@
    6.72          raise SAME ()
    6.73      | _ => raise SAME ())
    6.74     handle SAME () => Op3 (oper, T, R, u1, u2, u3))
    6.75 -  |> optimize_unit
    6.76  fun s_tuple T R us =
    6.77 -  (if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us))
    6.78 -  |> optimize_unit
    6.79 +  if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)
    6.80  
    6.81  fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
    6.82 -  | untuple f u = if rep_of u = Unit then [] else [f u]
    6.83 +  | untuple f u = [f u]
    6.84  
    6.85  fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
    6.86                         unsound table def =
    6.87 @@ -855,17 +845,14 @@
    6.88              Cst (if is_twos_complement_representable bits j then Num j
    6.89                   else Unrep, T, best_opt_set_rep_for_type scope T)
    6.90            else
    6.91 -            (case spec_of_type scope T of
    6.92 -               (1, j0) => if j = 0 then Cst (Unity, T, Unit)
    6.93 -                          else Cst (Unrep, T, Opt (Atom (1, j0)))
    6.94 -             | (k, j0) =>
    6.95 -               let
    6.96 -                 val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
    6.97 -                           else j < k)
    6.98 -               in
    6.99 -                 if ok then Cst (Num j, T, Atom (k, j0))
   6.100 -                 else Cst (Unrep, T, Opt (Atom (k, j0)))
   6.101 -               end)
   6.102 +             let
   6.103 +               val (k, j0) = spec_of_type scope T
   6.104 +               val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
   6.105 +                         else j < k)
   6.106 +             in
   6.107 +               if ok then Cst (Num j, T, Atom (k, j0))
   6.108 +               else Cst (Unrep, T, Opt (Atom (k, j0)))
   6.109 +             end
   6.110          | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
   6.111            let val R = Atom (spec_of_type scope T1) in
   6.112              Cst (Suc, T, Func (R, Opt R))
   6.113 @@ -1035,8 +1022,7 @@
   6.114            in s_op2 Apply T ran_R u1 u2 end
   6.115          | Op2 (Lambda, T, _, u1, u2) =>
   6.116            (case best_set_rep_for_type scope T of
   6.117 -             Unit => Cst (Unity, T, Unit)
   6.118 -           | R as Func (R1, _) =>
   6.119 +             R as Func (R1, _) =>
   6.120               let
   6.121                 val table' = NameTable.update (u1, R1) table
   6.122                 val u1' = aux table' false Neut u1
   6.123 @@ -1149,8 +1135,8 @@
   6.124            let
   6.125              val Rs = map (best_one_rep_for_type scope o type_of) us
   6.126              val us = map sub us
   6.127 -            val R = if forall (curry (op =) Unit) Rs then Unit else Struct Rs
   6.128 -            val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R
   6.129 +            val R' = Struct Rs
   6.130 +                     |> exists (is_opt_rep o rep_of) us ? opt_rep ofs T
   6.131            in s_tuple T R' us end
   6.132          | Construct (us', T, _, us) =>
   6.133            let
   6.134 @@ -1170,7 +1156,6 @@
   6.135                s_op1 Cast (type_of u) (Formula polar) u
   6.136            end
   6.137        end
   6.138 -      |> optimize_unit
   6.139    in aux table def Pos end
   6.140  
   6.141  fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys)
   6.142 @@ -1203,7 +1188,7 @@
   6.143      val w = constr (j, type_of v, rep_of v)
   6.144    in (w :: ws, pool, NameTable.update (v, w) table) end
   6.145  
   6.146 -fun shape_tuple (T as Type (@{type_name Product_Type.prod}, [T1, T2])) (R as Struct [R1, R2])
   6.147 +fun shape_tuple (T as Type (@{type_name prod}, [T1, T2])) (R as Struct [R1, R2])
   6.148                  us =
   6.149      let val arity1 = arity_of_rep R1 in
   6.150        Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
   6.151 @@ -1213,7 +1198,6 @@
   6.152      Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
   6.153    | shape_tuple T _ [u] =
   6.154      if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
   6.155 -  | shape_tuple T Unit [] = Cst (Unity, T, Unit)
   6.156    | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
   6.157  
   6.158  fun rename_n_ary_var rename_free v (ws, pool, table) =
   6.159 @@ -1259,7 +1243,6 @@
   6.160  
   6.161  fun rename_free_vars vs pool table =
   6.162    let
   6.163 -    val vs = filter (not_equal Unit o rep_of) vs
   6.164      val (vs, pool, table) = fold (rename_n_ary_var true) vs ([], pool, table)
   6.165    in (rev vs, pool, table) end
   6.166  
   6.167 @@ -1280,7 +1263,7 @@
   6.168        Op2 (oper, T, R, rename_vars_in_nut pool table u1,
   6.169             rename_vars_in_nut pool table u2)
   6.170    | Op3 (Let, T, R, u1, u2, u3) =>
   6.171 -    if rep_of u2 = Unit orelse inline_nut u2 then
   6.172 +    if inline_nut u2 then
   6.173        let
   6.174          val u2 = rename_vars_in_nut pool table u2
   6.175          val table = NameTable.update (u1, u2) table
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Aug 03 21:37:12 2010 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Aug 04 10:39:35 2010 +0200
     7.3 @@ -132,8 +132,8 @@
     7.4    let
     7.5      fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
     7.6          Type (@{type_name fun}, map box_relational_operator_type Ts)
     7.7 -      | box_relational_operator_type (Type (@{type_name Product_Type.prod}, Ts)) =
     7.8 -        Type (@{type_name Product_Type.prod}, map (box_type hol_ctxt InPair) Ts)
     7.9 +      | box_relational_operator_type (Type (@{type_name prod}, Ts)) =
    7.10 +        Type (@{type_name prod}, map (box_type hol_ctxt InPair) Ts)
    7.11        | box_relational_operator_type T = T
    7.12      fun add_boxed_types_for_var (z as (_, T)) (T', t') =
    7.13        case t' of
    7.14 @@ -1000,10 +1000,9 @@
    7.15      and add_axioms_for_type depth T =
    7.16        case T of
    7.17          Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
    7.18 -      | Type (@{type_name Product_Type.prod}, Ts) => fold (add_axioms_for_type depth) Ts
    7.19 +      | Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts
    7.20        | @{typ prop} => I
    7.21        | @{typ bool} => I
    7.22 -      | @{typ unit} => I
    7.23        | TFree (_, S) => add_axioms_for_sort depth T S
    7.24        | TVar (_, S) => add_axioms_for_sort depth T S
    7.25        | Type (z as (_, Ts)) =>
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Aug 03 21:37:12 2010 +0200
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Wed Aug 04 10:39:35 2010 +0200
     8.3 @@ -13,7 +13,6 @@
     8.4    datatype rep =
     8.5      Any |
     8.6      Formula of polarity |
     8.7 -    Unit |
     8.8      Atom of int * int |
     8.9      Struct of rep list |
    8.10      Vect of int * rep |
    8.11 @@ -68,7 +67,6 @@
    8.12  datatype rep =
    8.13    Any |
    8.14    Formula of polarity |
    8.15 -  Unit |
    8.16    Atom of int * int |
    8.17    Struct of rep list |
    8.18    Vect of int * rep |
    8.19 @@ -88,7 +86,6 @@
    8.20    end
    8.21  and string_for_rep Any = "X"
    8.22    | string_for_rep (Formula polar) = "F" ^ string_for_polarity polar
    8.23 -  | string_for_rep Unit = "U"
    8.24    | string_for_rep (Atom (k, j0)) =
    8.25      "A" ^ string_of_int k ^ (if j0 = 0 then "" else "@" ^ string_of_int j0)
    8.26    | string_for_rep (Struct rs) = "[" ^ commas (map string_for_rep rs) ^ "]"
    8.27 @@ -108,7 +105,6 @@
    8.28  
    8.29  fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any])
    8.30    | card_of_rep (Formula _) = 2
    8.31 -  | card_of_rep Unit = 1
    8.32    | card_of_rep (Atom (k, _)) = k
    8.33    | card_of_rep (Struct rs) = Integer.prod (map card_of_rep rs)
    8.34    | card_of_rep (Vect (k, R)) = reasonable_power (card_of_rep R) k
    8.35 @@ -117,7 +113,6 @@
    8.36    | card_of_rep (Opt R) = card_of_rep R
    8.37  fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any])
    8.38    | arity_of_rep (Formula _) = 0
    8.39 -  | arity_of_rep Unit = 0
    8.40    | arity_of_rep (Atom _) = 1
    8.41    | arity_of_rep (Struct Rs) = Integer.sum (map arity_of_rep Rs)
    8.42    | arity_of_rep (Vect (k, R)) = k * arity_of_rep R
    8.43 @@ -126,7 +121,6 @@
    8.44  fun min_univ_card_of_rep Any =
    8.45      raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any])
    8.46    | min_univ_card_of_rep (Formula _) = 0
    8.47 -  | min_univ_card_of_rep Unit = 0
    8.48    | min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1
    8.49    | min_univ_card_of_rep (Struct Rs) =
    8.50      fold Integer.max (map min_univ_card_of_rep Rs) 0
    8.51 @@ -135,8 +129,7 @@
    8.52      Int.max (min_univ_card_of_rep R1, min_univ_card_of_rep R2)
    8.53    | min_univ_card_of_rep (Opt R) = min_univ_card_of_rep R
    8.54  
    8.55 -fun is_one_rep Unit = true
    8.56 -  | is_one_rep (Atom _) = true
    8.57 +fun is_one_rep (Atom _) = true
    8.58    | is_one_rep (Struct _) = true
    8.59    | is_one_rep (Vect _) = true
    8.60    | is_one_rep _ = false
    8.61 @@ -145,8 +138,7 @@
    8.62  
    8.63  fun dest_Func (Func z) = z
    8.64    | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
    8.65 -fun lazy_range_rep _ _ _ Unit = Unit
    8.66 -  | lazy_range_rep _ _ _ (Vect (_, R)) = R
    8.67 +fun lazy_range_rep _ _ _ (Vect (_, R)) = R
    8.68    | lazy_range_rep _ _ _ (Func (_, R2)) = R2
    8.69    | lazy_range_rep ofs T ran_card (Opt R) =
    8.70      Opt (lazy_range_rep ofs T ran_card R)
    8.71 @@ -201,8 +193,6 @@
    8.72      Formula (min_polarity polar1 polar2)
    8.73    | min_rep (Formula polar) _ = Formula polar
    8.74    | min_rep _ (Formula polar) = Formula polar
    8.75 -  | min_rep Unit _ = Unit
    8.76 -  | min_rep _ Unit = Unit
    8.77    | min_rep (Atom x) _ = Atom x
    8.78    | min_rep _ (Atom x) = Atom x
    8.79    | min_rep (Struct Rs1) (Struct Rs2) = Struct (min_reps Rs1 Rs2)
    8.80 @@ -231,8 +221,7 @@
    8.81  
    8.82  fun card_of_domain_from_rep ran_card R =
    8.83    case R of
    8.84 -    Unit => 1
    8.85 -  | Atom (k, _) => exact_log ran_card k
    8.86 +    Atom (k, _) => exact_log ran_card k
    8.87    | Vect (k, _) => k
    8.88    | Func (R1, _) => card_of_rep R1
    8.89    | Opt R => card_of_domain_from_rep ran_card R
    8.90 @@ -246,24 +235,12 @@
    8.91  
    8.92  fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
    8.93                            (Type (@{type_name fun}, [T1, T2])) =
    8.94 -    (case best_one_rep_for_type scope T2 of
    8.95 -       Unit => Unit
    8.96 -     | R2 => Vect (card_of_type card_assigns T1, R2))
    8.97 -  | best_one_rep_for_type scope (Type (@{type_name Product_Type.prod}, [T1, T2])) =
    8.98 -    (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
    8.99 -       (Unit, Unit) => Unit
   8.100 -     | (R1, R2) => Struct [R1, R2])
   8.101 +    Vect (card_of_type card_assigns T1, (best_one_rep_for_type scope T2))
   8.102 +  | best_one_rep_for_type scope (Type (@{type_name prod}, Ts)) =
   8.103 +    Struct (map (best_one_rep_for_type scope) Ts)
   8.104    | best_one_rep_for_type {card_assigns, datatypes, ofs, ...} T =
   8.105 -    (case card_of_type card_assigns T of
   8.106 -       1 => if is_some (datatype_spec datatypes T) orelse
   8.107 -               is_iterator_type T then
   8.108 -              Atom (1, offset_of_type ofs T)
   8.109 -            else
   8.110 -              Unit
   8.111 -     | k => Atom (k, offset_of_type ofs T))
   8.112 +    Atom (card_of_type card_assigns T, offset_of_type ofs T)
   8.113  
   8.114 -(* Datatypes are never represented by Unit, because it would confuse
   8.115 -   "nfa_transitions_for_ctor". *)
   8.116  fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
   8.117      Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
   8.118    | best_opt_set_rep_for_type (scope as {ofs, ...}) T =
   8.119 @@ -272,10 +249,7 @@
   8.120                                    (Type (@{type_name fun}, [T1, T2])) =
   8.121      (case (best_one_rep_for_type scope T1,
   8.122             best_non_opt_set_rep_for_type scope T2) of
   8.123 -       (_, Unit) => Unit
   8.124 -     | (Unit, Atom (2, _)) =>
   8.125 -       Func (Atom (1, offset_of_type ofs T1), Formula Neut)
   8.126 -     | (R1, Atom (2, _)) => Func (R1, Formula Neut)
   8.127 +       (R1, Atom (2, _)) => Func (R1, Formula Neut)
   8.128       | z => Func z)
   8.129    | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
   8.130  fun best_set_rep_for_type (scope as {datatypes, ...}) T =
   8.131 @@ -290,7 +264,6 @@
   8.132  
   8.133  fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any])
   8.134    | atom_schema_of_rep (Formula _) = []
   8.135 -  | atom_schema_of_rep Unit = []
   8.136    | atom_schema_of_rep (Atom x) = [x]
   8.137    | atom_schema_of_rep (Struct Rs) = atom_schema_of_reps Rs
   8.138    | atom_schema_of_rep (Vect (k, R)) = replicate_list k (atom_schema_of_rep R)
   8.139 @@ -300,9 +273,8 @@
   8.140  and atom_schema_of_reps Rs = maps atom_schema_of_rep Rs
   8.141  
   8.142  fun type_schema_of_rep _ (Formula _) = []
   8.143 -  | type_schema_of_rep _ Unit = []
   8.144    | type_schema_of_rep T (Atom _) = [T]
   8.145 -  | type_schema_of_rep (Type (@{type_name Product_Type.prod}, [T1, T2])) (Struct [R1, R2]) =
   8.146 +  | type_schema_of_rep (Type (@{type_name prod}, [T1, T2])) (Struct [R1, R2]) =
   8.147      type_schema_of_reps [T1, T2] [R1, R2]
   8.148    | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
   8.149      replicate_list k (type_schema_of_rep T2 R)
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Aug 03 21:37:12 2010 +0200
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Aug 04 10:39:35 2010 +0200
     9.3 @@ -114,7 +114,7 @@
     9.4      is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
     9.5    | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
     9.6      is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
     9.7 -  | is_complete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
     9.8 +  | is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) =
     9.9      forall (is_complete_type dtypes facto) Ts
    9.10    | is_complete_type dtypes facto T =
    9.11      not (is_integer_like_type T) andalso not (is_bit_type T) andalso
    9.12 @@ -124,7 +124,7 @@
    9.13      is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
    9.14    | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
    9.15      is_concrete_type dtypes facto T2
    9.16 -  | is_concrete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) =
    9.17 +  | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) =
    9.18      forall (is_concrete_type dtypes facto) Ts
    9.19    | is_concrete_type dtypes facto T =
    9.20      fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Aug 03 21:37:12 2010 +0200
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Wed Aug 04 10:39:35 2010 +0200
    10.3 @@ -23,10 +23,8 @@
    10.4  
    10.5  fun cast_to_rep R u = Op1 (Cast, type_of u, R, u)
    10.6  
    10.7 -val unit_T = @{typ unit}
    10.8  val dummy_T = @{typ 'a}
    10.9  
   10.10 -val unity = Cst (Unity, unit_T, Unit)
   10.11  val atom1_v1 = FreeName ("atom1_v1", dummy_T, Atom (1, 0))
   10.12  val atom2_v1 = FreeName ("atom2_v1", dummy_T, Atom (2, 0))
   10.13  val atom6_v1 = FreeName ("atom6_v1", dummy_T, Atom (6, 0))
   10.14 @@ -36,19 +34,14 @@
   10.15  val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0))
   10.16  val struct_atom1_atom1_v1 =
   10.17    FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])
   10.18 -val struct_atom1_unit_v1 =
   10.19 -  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Unit])
   10.20 -val struct_unit_atom1_v1 =
   10.21 -  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Unit, Atom (1, 0)])
   10.22  
   10.23  (*
   10.24 -              Formula    Unit   Atom    Struct    Vect    Func
   10.25 -    Formula      X       N/A     X        X       N/A     N/A
   10.26 -    Unit        N/A      N/A    N/A      N/A      N/A     N/A
   10.27 -    Atom         X       N/A     X        X        X       X
   10.28 -    Struct      N/A      N/A     X        X       N/A     N/A
   10.29 -    Vect        N/A      N/A     X       N/A       X       X
   10.30 -    Func        N/A      N/A     X       N/A       X       X
   10.31 +              Formula    Atom    Struct    Vect    Func
   10.32 +    Formula      X       X        X       N/A     N/A
   10.33 +    Atom         X       X        X        X       X
   10.34 +    Struct      N/A      X        X       N/A     N/A
   10.35 +    Vect        N/A      X       N/A       X       X
   10.36 +    Func        N/A      X       N/A       X       X
   10.37  *)
   10.38  
   10.39  val tests =
   10.40 @@ -77,22 +70,6 @@
   10.41                                     Struct [Atom (2, 0), Atom (3, 0)]])
   10.42                            atom24_v1),
   10.43           atom24_v1)),
   10.44 -   ("rep_conversion_struct_struct_4",
   10.45 -    Op2 (Eq, bool_T, Formula Neut,
   10.46 -         cast_to_rep (Struct [Atom (24, 0), Unit])
   10.47 -             (cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)]) atom24_v1),
   10.48 -         atom24_v1)),
   10.49 -   ("rep_conversion_struct_struct_5",
   10.50 -    Op2 (Eq, bool_T, Formula Neut,
   10.51 -         cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)])
   10.52 -             (cast_to_rep (Struct [Atom (24, 0), Unit]) atom24_v1),
   10.53 -         atom24_v1)),
   10.54 -   ("rep_conversion_struct_struct_6",
   10.55 -    Op2 (Eq, bool_T, Formula Neut,
   10.56 -         cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)])
   10.57 -             (cast_to_rep (Struct [Atom (1, 0), Unit])
   10.58 -                 (cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1)),
   10.59 -         atom1_v1)),
   10.60     ("rep_conversion_vect_vect_1",
   10.61      Op2 (Eq, bool_T, Formula Neut,
   10.62           cast_to_rep (Atom (16, 0))
   10.63 @@ -133,50 +110,10 @@
   10.64                                  Struct [Atom (2, 0), Atom (3, 0)]))
   10.65                         atom36_v1)),
   10.66           atom36_v1)),
   10.67 -   ("rep_conversion_func_func_3",
   10.68 -    Op2 (Eq, bool_T, Formula Neut,
   10.69 -         cast_to_rep (Atom (36, 0))
   10.70 -             (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
   10.71 -                  (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
   10.72 -         atom36_v1)),
   10.73 -   ("rep_conversion_func_func_4",
   10.74 -    Op2 (Eq, bool_T, Formula Neut,
   10.75 -         cast_to_rep (Atom (36, 0))
   10.76 -             (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
   10.77 -                  (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
   10.78 -                       atom36_v1)),
   10.79 -         atom36_v1)),
   10.80 -   ("rep_conversion_func_func_5",
   10.81 -    Op2 (Eq, bool_T, Formula Neut,
   10.82 -         cast_to_rep (Atom (36, 0))
   10.83 -             (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
   10.84 -                  (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
   10.85 -         atom36_v1)),
   10.86 -   ("rep_conversion_func_func_6",
   10.87 -    Op2 (Eq, bool_T, Formula Neut,
   10.88 -         cast_to_rep (Atom (36, 0))
   10.89 -             (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
   10.90 -                  (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
   10.91 -                       atom36_v1)),
   10.92 -         atom36_v1)),
   10.93 -   ("rep_conversion_func_func_7",
   10.94 -    Op2 (Eq, bool_T, Formula Neut,
   10.95 -         cast_to_rep (Atom (2, 0))
   10.96 -             (cast_to_rep (Func (Unit, Atom (2, 0)))
   10.97 -                  (cast_to_rep (Func (Atom (1, 0), Formula Neut)) atom2_v1)),
   10.98 -         atom2_v1)),
   10.99 -   ("rep_conversion_func_func_8",
  10.100 -    Op2 (Eq, bool_T, Formula Neut,
  10.101 -         cast_to_rep (Atom (2, 0))
  10.102 -             (cast_to_rep (Func (Atom (1, 0), Formula Neut))
  10.103 -                  (cast_to_rep (Func (Unit, Atom (2, 0))) atom2_v1)),
  10.104 -         atom2_v1)),
  10.105     ("rep_conversion_atom_formula_atom",
  10.106      Op2 (Eq, bool_T, Formula Neut,
  10.107           cast_to_rep (Atom (2, 0)) (cast_to_rep (Formula Neut) atom2_v1),
  10.108           atom2_v1)),
  10.109 -   ("rep_conversion_unit_atom",
  10.110 -    Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (1, 0)) unity, unity)),
  10.111     ("rep_conversion_atom_struct_atom1",
  10.112      Op2 (Eq, bool_T, Formula Neut,
  10.113           cast_to_rep (Atom (6, 0))
  10.114 @@ -188,17 +125,6 @@
  10.115               (cast_to_rep (Struct [Struct [Atom (3, 0), Atom (4, 0)],
  10.116                                     Atom (2, 0)]) atom24_v1),
  10.117           atom24_v1)),
  10.118 -   ("rep_conversion_atom_struct_atom_3",
  10.119 -    Op2 (Eq, bool_T, Formula Neut,
  10.120 -         cast_to_rep (Atom (6, 0))
  10.121 -                     (cast_to_rep (Struct [Atom (6, 0), Unit]) atom6_v1),
  10.122 -         atom6_v1)),
  10.123 -   ("rep_conversion_atom_struct_atom_4",
  10.124 -    Op2 (Eq, bool_T, Formula Neut,
  10.125 -         cast_to_rep (Atom (6, 0))
  10.126 -             (cast_to_rep (Struct [Struct [Atom (3, 0), Unit], Atom (2, 0)]) 
  10.127 -             atom6_v1),
  10.128 -         atom6_v1)),
  10.129     ("rep_conversion_atom_vect_func_atom_1",
  10.130      Op2 (Eq, bool_T, Formula Neut,
  10.131           cast_to_rep (Atom (16, 0))
  10.132 @@ -217,18 +143,6 @@
  10.133               (cast_to_rep (Vect (4, Atom (2, 0)))
  10.134                    (cast_to_rep (Func (Atom (4, 0), Formula Neut)) atom16_v1)),
  10.135           atom16_v1)),
  10.136 -   ("rep_conversion_atom_vect_func_atom_4",
  10.137 -    Op2 (Eq, bool_T, Formula Neut,
  10.138 -         cast_to_rep (Atom (16, 0))
  10.139 -             (cast_to_rep (Vect (1, Atom (16, 0)))
  10.140 -                  (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
  10.141 -         atom16_v1)),
  10.142 -   ("rep_conversion_atom_vect_func_atom_5",
  10.143 -    Op2 (Eq, bool_T, Formula Neut,
  10.144 -         cast_to_rep (Atom (16, 0))
  10.145 -             (cast_to_rep (Vect (1, Atom (16, 0)))
  10.146 -                  (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
  10.147 -         atom16_v1)),
  10.148     ("rep_conversion_atom_func_vect_atom_1",
  10.149      Op2 (Eq, bool_T, Formula Neut,
  10.150           cast_to_rep (Atom (16, 0))
  10.151 @@ -247,12 +161,6 @@
  10.152               (cast_to_rep (Func (Atom (4, 0), Formula Neut))
  10.153                    (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
  10.154           atom16_v1)),
  10.155 -   ("rep_conversion_atom_func_vect_atom_4",
  10.156 -    Op2 (Eq, bool_T, Formula Neut,
  10.157 -         cast_to_rep (Atom (16, 0))
  10.158 -             (cast_to_rep (Func (Unit, Atom (16, 0)))
  10.159 -                  (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)),
  10.160 -         atom16_v1)),
  10.161     ("rep_conversion_atom_func_vect_atom_5",
  10.162      Op2 (Eq, bool_T, Formula Neut,
  10.163           cast_to_rep (Atom (16, 0))
  10.164 @@ -274,23 +182,7 @@
  10.165     ("rep_conversion_struct_atom1_1",
  10.166      Op2 (Eq, bool_T, Formula Neut,
  10.167           cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)]) atom1_v1,
  10.168 -                      struct_atom1_atom1_v1)),
  10.169 -   ("rep_conversion_struct_atom1_2",
  10.170 -    Op2 (Eq, bool_T, Formula Neut,
  10.171 -         cast_to_rep (Struct [Atom (1, 0), Unit]) atom1_v1,
  10.172 -                      struct_atom1_unit_v1)),
  10.173 -   ("rep_conversion_struct_atom1_3",
  10.174 -    Op2 (Eq, bool_T, Formula Neut,
  10.175 -         cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1,
  10.176 -                      struct_unit_atom1_v1))
  10.177 -(*
  10.178 -   ("rep_conversion_struct_formula_struct_1",
  10.179 -    Op2 (Eq, bool_T, Formula Neut,
  10.180 -         cast_to_rep (Struct [Atom (2, 0), Unit])
  10.181 -             (cast_to_rep (Formula Neut) struct_atom_2_unit_v1),
  10.182 -         struct_atom_2_unit_v1))
  10.183 -*)
  10.184 -  ]
  10.185 +                      struct_atom1_atom1_v1))]
  10.186  
  10.187  fun problem_for_nut ctxt (name, u) =
  10.188    let
  10.189 @@ -319,13 +211,14 @@
  10.190  
  10.191  fun run_all_tests () =
  10.192    let
  10.193 -    val {overlord, ...} = Nitpick_Isar.default_params thy []
  10.194 +    val {overlord, ...} = Nitpick_Isar.default_params @{theory} []
  10.195      val max_threads = 1
  10.196      val max_solutions = 1
  10.197    in
  10.198      case Kodkod.solve_any_problem overlord NONE max_threads max_solutions
  10.199                                    (map (problem_for_nut @{context}) tests) of
  10.200 -    Kodkod.Normal ([], _, _) => ()
  10.201 -  | _ => error "Tests failed."
  10.202 +      Kodkod.Normal ([], _, _) => ()
  10.203 +    | _ => error "Tests failed."
  10.204 +  end
  10.205  
  10.206  end;