src/Tools/nbe.ML

 
 (** evaluation **)
 
 (* term evaluation *)
 
-fun eval_term ctxt gr deps ((vs, ty), t) =
+fun eval_term ctxt gr deps ((vs, ty) : typscheme, t) =
   let 
     val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t []
     val frees' = map (fn v => Free (v, [])) frees;
     val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   in