src/HOL/Tools/Nitpick/nitpick_mono.ML

 
 type mtype_schema = mtyp * constraint_set
 type mtype_context =
   {bound_Ts: typ list,
    bound_Ms: mtyp list,
+   bound_frame: (int * annotation_atom) list,
    frees: (styp * mtyp) list,
    consts: (styp * mtyp) list}
 
 type accumulator = mtype_context * constraint_set
 
-val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []}
-
-fun push_bound T M {bound_Ts, bound_Ms, frees, consts} =
-  {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees,
-   consts = consts}
-fun pop_bound {bound_Ts, bound_Ms, frees, consts} =
-  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees,
-   consts = consts}
+val initial_gamma =
+  {bound_Ts = [], bound_Ms = [], bound_frame = [], frees = [], consts = []}
+
+fun push_bound T M {bound_Ts, bound_Ms, bound_frame, frees, consts} =
+  {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms,
+   bound_frame = bound_frame, frees = frees, consts = consts}
+fun pop_bound {bound_Ts, bound_Ms, bound_frame, frees, consts} =
+  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, bound_frame = bound_frame,
+   frees = frees, consts = consts}
   handle List.Empty => initial_gamma (* FIXME: needed? *)
 
 fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
                              max_fresh, ...}) =
   let

                      MApp (MApp (MRaw (connective_t,
                                        mtype_for (fastype_of connective_t)),
                                  MApp (bound_m, MRaw (Bound 0, M1))),
                            body_m))), accum)
       end
-    and do_term t (accum as ({bound_Ts, bound_Ms, frees, consts}, cset)) =
+    and do_term t (accum as ({bound_Ts, bound_Ms, bound_frame, frees, consts},
+                             cset)) =
         (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
                              Syntax.string_of_term ctxt t ^ " : _?");
          case t of
            Const (x as (s, T)) =>
            (case AList.lookup (op =) consts x of

                 else if is_built_in_const thy stds x then
                   (fresh_mtype_for_type mdata true T, accum)
                 else
                   let val M = mtype_for T in
                     (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
-                          frees = frees, consts = (x, M) :: consts}, cset))
+                          bound_frame = bound_frame, frees = frees,
+                          consts = (x, M) :: consts}, cset))
                   end) |>> curry MRaw t
          | Free (x as (_, T)) =>
            (case AList.lookup (op =) frees x of
               SOME M => (M, accum)
             | NONE =>
               let val M = mtype_for T in
                 (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
-                      frees = (x, M) :: frees, consts = consts}, cset))
+                      bound_frame = bound_frame, frees = (x, M) :: frees,
+                      consts = consts}, cset))
               end) |>> curry MRaw t
          | Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
          | Bound j => (MRaw (t, nth bound_Ms j), accum)
          | Abs (s, T, t') =>
            (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of