--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 19:31:00 2010 +0100
@@ -293,8 +293,8 @@
$ 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