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", [_, T2])) =>
-        let val T' = box_type hol_ctxt InSel T2 in
+      | 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