1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jun 01 15:53:15 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jun 01 16:17:46 2010 +0200
     1.3 @@ -1055,11 +1055,11 @@
     1.4            (s, case AList.lookup (op =) constr_mtypes x of
     1.5                  SOME M => type_from_mtype T M
     1.6                | NONE => T)
     1.7 -        fun term_from_mterm Ts m =
     1.8 +        fun term_from_mterm new_Ts old_Ts m =
     1.9            case m of
    1.10              MRaw (t, M) =>
    1.11              let
    1.12 -              val T = fastype_of1 (Ts, t)
    1.13 +              val T = fastype_of1 (old_Ts, t)
    1.14                val T' = type_from_mtype T M
    1.15              in
    1.16                case t of
    1.17 @@ -1073,7 +1073,7 @@
    1.18                            $ (Const (@{const_name is_unknown},
    1.19                                      elem_T' --> bool_T) $ Bound 1)
    1.20                            $ (Const (@{const_name unknown}, set_T'))
    1.21 -                          $ (coerce_term hol_ctxt Ts T' T (Const x)
    1.22 +                          $ (coerce_term hol_ctxt new_Ts T' T (Const x)
    1.23                               $ Bound 1 $ Bound 0)))
    1.24                    | _ => Const (s, T')
    1.25                  else if s = @{const_name finite} then
    1.26 @@ -1085,7 +1085,7 @@
    1.27                          s = @{const_name "op ="} then
    1.28                    Const (s, T')
    1.29                  else if is_built_in_const thy stds fast_descrs x then
    1.30 -                  coerce_term hol_ctxt Ts T' T t
    1.31 +                  coerce_term hol_ctxt new_Ts T' T t
    1.32                  else if is_constr ctxt stds x then
    1.33                    Const (finitize_constr x)
    1.34                  else if is_sel s then
    1.35 @@ -1107,8 +1107,8 @@
    1.36              end
    1.37            | MApp (m1, m2) =>
    1.38              let
    1.39 -              val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
    1.40 -              val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
    1.41 +              val (t1, t2) = pairself (term_from_mterm new_Ts old_Ts) (m1, m2)
    1.42 +              val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
    1.43                val (t1', T2') =
    1.44                  case T1 of
    1.45                    Type (s, [T11, T12]) => 
    1.46 @@ -1119,20 +1119,20 @@
    1.47                       t1, T11)
    1.48                  | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
    1.49                                     [T1], [])
    1.50 -            in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
    1.51 -          | MAbs (s, T, M, a, m') =>
    1.52 +            in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end
    1.53 +          | MAbs (s, old_T, M, a, m') =>
    1.54              let
    1.55 -              val T = type_from_mtype T M
    1.56 -              val t' = term_from_mterm (T :: Ts) m'
    1.57 -              val T' = fastype_of1 (T :: Ts, t')
    1.58 +              val new_T = type_from_mtype old_T M
    1.59 +              val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
    1.60 +              val T' = fastype_of1 (new_T :: new_Ts, t')
    1.61              in
    1.62 -              Abs (s, T, t')
    1.63 -              |> should_finitize (T --> T') a
    1.64 -                 ? construct_value ctxt stds (fin_fun_constr T T') o single
    1.65 +              Abs (s, new_T, t')
    1.66 +              |> should_finitize (new_T --> T') a
    1.67 +                 ? construct_value ctxt stds (fin_fun_constr new_T T') o single
    1.68              end
    1.69        in
    1.70          Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
    1.71 -        pairself (map (term_from_mterm [])) msp
    1.72 +        pairself (map (term_from_mterm [] [])) msp
    1.73        end
    1.74    | NONE => tsp
    1.75