src/HOL/Tools/Nitpick/nitpick_preproc.ML

       | @{const "op -->"} $ t1 $ t2 =>
         @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
         $ 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
                   else if is_constr_like thy x then
                     box_type hol_ctxt InConstr T

 (* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
 val axioms_max_depth = 255
 
 (* 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)
        -> ((term list -> term list) -> term list * term list
            -> term list * term list)

       | Type (z as (_, Ts)) =>
         fold (add_axioms_for_type depth) Ts
         #> (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)
             else
               I)