guard against unsound cases that arise when people peek into 'int' and similar types that are handled specially by Nitpick

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 12:58:17 2014 +0100
@@ -1775,17 +1775,24 @@
                 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
                                      \(\"" ^ s ^ "\")")
               else if is_quot_abs_fun ctxt x then
-                let
-                  val rep_T = domain_type T
-                  val abs_T = range_type T
-                in
-                  (Abs (Name.uu, rep_T,
-                        Const (@{const_name Quot}, rep_T --> abs_T)
-                               $ (Const (quot_normal_name_for_type ctxt abs_T,
-                                         rep_T --> rep_T) $ Bound 0)), ts)
-                end
+                case T of
+                  Type (@{type_name fun}, [rep_T, abs_T as Type (abs_s, _)]) =>
+                  if is_basic_datatype thy [(NONE, true)] abs_s then
+                    raise NOT_SUPPORTED ("abstraction function on " ^
+                                         quote abs_s)
+                  else
+                    (Abs (Name.uu, rep_T,
+                          Const (@{const_name Quot}, rep_T --> abs_T)
+                                 $ (Const (quot_normal_name_for_type ctxt abs_T,
+                                           rep_T --> rep_T) $ Bound 0)), ts)
               else if is_quot_rep_fun ctxt x then
-                quot_rep_of depth Ts (domain_type T) (range_type T) ts
+                case T of
+                  Type (@{type_name fun}, [abs_T as Type (abs_s, _), rep_T]) =>
+                  if is_basic_datatype thy [(NONE, true)] abs_s then
+                    raise NOT_SUPPORTED ("representation function on " ^
+                                         quote abs_s)
+                  else
+                    quot_rep_of depth Ts abs_T rep_T ts
               else if is_record_get thy x then
                 case length ts of
                   0 => (do_term depth Ts (eta_expand Ts t 1), [])