Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
be more explicit: made sml/nj happy
authorhaftmann
Thu, 05 Jun 2014 11:11:41 +0200
changeset 57174 db969ff6a8b3
parent 57173 897cc57a6f55
child 57175 ca3475504557
be more explicit: made sml/nj happy
src/Tools/nbe.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle