# HG changeset patch
# User haftmann
# Date 1401959501 -7200
# Node ID db969ff6a8b30a1a10550938f965d9dbef57e22d
# Parent  897cc57a6f553ba9a421c8099b245785dc416c7c
be more explicit: made sml/nj happy

diff -r 897cc57a6f55 -r db969ff6a8b3 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);