src/Tools/nbe.ML

--- a/src/Tools/nbe.ML	Thu Jun 05 10:52:19 2014 +0200
+++ b/src/Tools/nbe.ML	Thu Jun 05 11:11:41 2014 +0200
@@ -536,7 +536,7 @@
 
 (* evaluation with type reconstruction *)
 
-fun eval_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty), t) deps =
+fun eval_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps =
   let
     val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
     val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);