1.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 08 15:20:40 2010 -0800
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Mar 09 09:25:23 2010 +0100
     1.3 @@ -287,8 +287,9 @@
     1.4         "Tuple " ^ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^
     1.5         implode (map sub us)
     1.6       | Construct (us', T, R, us) =>
     1.7 -       "Construct " ^ implode (map sub us') ^ Syntax.string_of_typ ctxt T ^
     1.8 -       " " ^ string_for_rep R ^ " " ^ implode (map sub us)
     1.9 +       "Construct " ^ implode (map sub us') ^ " " ^
    1.10 +       Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
    1.11 +       implode (map sub us)
    1.12       | BoundName (j, T, R, nick) =>
    1.13         "BoundName " ^ signed_string_of_int j ^ " " ^
    1.14         Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
    1.15 @@ -459,7 +460,8 @@
    1.16        (res_T, Const (@{const_name snd}, T --> res_T) $ t)
    1.17      end
    1.18  (* typ * term -> (typ * term) list *)
    1.19 -fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
    1.20 +fun factorize (z as (Type (@{type_name "*"}, _), _)) =
    1.21 +    maps factorize [mk_fst z, mk_snd z]
    1.22    | factorize z = [z]
    1.23  
    1.24  (* hol_context -> op2 -> term -> nut *)
    1.25 @@ -623,7 +625,8 @@
    1.26            if is_built_in_const thy stds false x then Cst (Add, T, Any)
    1.27            else ConstName (s, T, Any)
    1.28          | (Const (@{const_name minus_class.minus},
    1.29 -                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
    1.30 +                  Type (@{type_name fun},
    1.31 +                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
    1.32             [t1, t2]) =>
    1.33            Op2 (SetDifference, T1, Any, sub t1, sub t2)
    1.34          | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
    1.35 @@ -642,7 +645,8 @@
    1.36            else
    1.37              do_apply t0 ts
    1.38          | (Const (@{const_name ord_class.less_eq},
    1.39 -                  Type ("fun", [Type ("fun", [_, @{typ bool}]), _])),
    1.40 +                  Type (@{type_name fun},
    1.41 +                        [Type (@{type_name fun}, [_, @{typ bool}]), _])),
    1.42             [t1, t2]) =>
    1.43            Op2 (Subset, bool_T, Any, sub t1, sub t2)
    1.44          (* FIXME: find out if this case is necessary *)
    1.45 @@ -666,7 +670,7 @@
    1.46          | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
    1.47          | (Const (@{const_name is_unknown}, _), [t1]) =>
    1.48            Op1 (IsUnknown, bool_T, Any, sub t1)
    1.49 -        | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
    1.50 +        | (Const (@{const_name Tha}, Type (@{type_name fun}, [_, T2])), [t1]) =>
    1.51            Op1 (Tha, T2, Any, sub t1)
    1.52          | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
    1.53          | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
    1.54 @@ -676,11 +680,13 @@
    1.55                    T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
    1.56            Cst (NatToInt, T, Any)
    1.57          | (Const (@{const_name semilattice_inf_class.inf},
    1.58 -                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
    1.59 +                  Type (@{type_name fun},
    1.60 +                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
    1.61             [t1, t2]) =>
    1.62            Op2 (Intersect, T1, Any, sub t1, sub t2)
    1.63          | (Const (@{const_name semilattice_sup_class.sup},
    1.64 -                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
    1.65 +                  Type (@{type_name fun},
    1.66 +                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
    1.67             [t1, t2]) =>
    1.68            Op2 (Union, T1, Any, sub t1, sub t2)
    1.69          | (t0 as Const (x as (s, T)), ts) =>
    1.70 @@ -956,7 +962,7 @@
    1.71                   if ok then Cst (Num j, T, Atom (k, j0))
    1.72                   else Cst (Unrep, T, Opt (Atom (k, j0)))
    1.73                 end)
    1.74 -        | Cst (Suc, T as Type ("fun", [T1, _]), _) =>
    1.75 +        | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
    1.76            let val R = Atom (spec_of_type scope T1) in
    1.77              Cst (Suc, T, Func (R, Opt R))
    1.78            end
    1.79 @@ -1306,12 +1312,13 @@
    1.80    in (w :: ws, pool, NameTable.update (v, w) table) end
    1.81  
    1.82  (* typ -> rep -> nut list -> nut *)
    1.83 -fun shape_tuple (T as Type ("*", [T1, T2])) (R as Struct [R1, R2]) us =
    1.84 +fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2])
    1.85 +                us =
    1.86      let val arity1 = arity_of_rep R1 in
    1.87        Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
    1.88                      shape_tuple T2 R2 (List.drop (us, arity1))])
    1.89      end
    1.90 -  | shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
    1.91 +  | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
    1.92      Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
    1.93    | shape_tuple T _ [u] =
    1.94      if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])