1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 22 14:36:10 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 22 19:31:00 2010 +0100
     1.3 @@ -293,8 +293,8 @@
     1.4          $ do_term new_Ts old_Ts polar t2
     1.5        | Const (s as @{const_name The}, T) => do_description_operator s T
     1.6        | Const (s as @{const_name Eps}, T) => do_description_operator s T
     1.7 -      | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
     1.8 -        let val T' = box_type hol_ctxt InSel T2 in
     1.9 +      | Const (@{const_name quot_normal}, Type ("fun", [T, _])) =>
    1.10 +        let val T' = box_type hol_ctxt InFunLHS T in
    1.11            Const (@{const_name quot_normal}, T' --> T')
    1.12          end
    1.13        | Const (s as @{const_name Tha}, T) => do_description_operator s T