diff -r 997aa3a3e4bb -r 8f9a66fc9f80 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 23 10:02:14 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 23 11:05:32 2010 +0100
@@ -293,15 +293,15 @@
         $ do_term new_Ts old_Ts polar t2
       | Const (s as @{const_name The}, T) => do_description_operator s T
       | Const (s as @{const_name Eps}, T) => do_description_operator s T
-      | Const (@{const_name quot_normal}, Type ("fun", [T, _])) =>
-        let val T' = box_type hol_ctxt InFunLHS T in
-          Const (@{const_name quot_normal}, T' --> T')
-        end
       | Const (s as @{const_name Tha}, T) => do_description_operator s T
       | Const (x as (s, T)) =>
         Const (s, if s = @{const_name converse} orelse
                      s = @{const_name trancl} then
                     box_relational_operator_type T
+                  else if String.isPrefix quot_normal_prefix s then
+                    let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
+                      T' --> T'
+                    end
                   else if is_built_in_const thy stds fast_descrs x orelse
                           s = @{const_name Sigma} then
                     T
@@ -1022,8 +1022,9 @@
 
 (* hol_context -> term -> (term list * term list) * (bool * bool) *)
 fun axioms_for_term
-        (hol_ctxt as {thy, max_bisim_depth, stds, user_axioms, fast_descrs,
-                      evals, def_table, nondef_table, user_nondefs, ...}) t =
+        (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
+                      fast_descrs, evals, def_table, nondef_table, user_nondefs,
+                      ...}) t =
   let
     type accumulator = styp list * (term list * term list)
     (* (term list * term list -> term list)
@@ -1134,7 +1135,8 @@
         #> (if is_pure_typedef thy T then
               fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
             else if is_quot_type thy T then
-              fold (add_def_axiom depth) (optimized_quot_type_axioms thy stds z)
+              fold (add_def_axiom depth)
+                   (optimized_quot_type_axioms ctxt stds z)
             else if max_bisim_depth >= 0 andalso is_codatatype thy T then
               fold (add_maybe_def_axiom depth)
                    (codatatype_bisim_axioms hol_ctxt T)