src/Pure/type_infer_context.ML
changeset 43278 1fbdcebb364b
parent 42405 13ecdb3057d8
child 45429 fd58cbf8cae3
     1.1 --- a/src/Pure/type_infer_context.ML	Wed Jun 08 15:39:55 2011 +0200
     1.2 +++ b/src/Pure/type_infer_context.ML	Wed Jun 08 15:56:57 2011 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4        | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
     1.5        | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
     1.6        | inf bs (Bound i) tye_idx =
     1.7 -          (snd (nth bs i handle Subscript => err_loose i), tye_idx)
     1.8 +          (snd (nth bs i handle General.Subscript => err_loose i), tye_idx)
     1.9        | inf bs (Abs (x, T, t)) tye_idx =
    1.10            let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
    1.11            in (T --> U, tye_idx') end