be more explicit: made sml/nj happy
authorhaftmann
Thu Jun 05 11:11:41 2014 +0200 (2014-06-05)
changeset 57174db969ff6a8b3
parent 57173 897cc57a6f55
child 57175 ca3475504557
be more explicit: made sml/nj happy
src/Tools/nbe.ML
     1.1 --- a/src/Tools/nbe.ML	Thu Jun 05 10:52:19 2014 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu Jun 05 11:11:41 2014 +0200
     1.3 @@ -536,7 +536,7 @@
     1.4  
     1.5  (* evaluation with type reconstruction *)
     1.6  
     1.7 -fun eval_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty), t) deps =
     1.8 +fun eval_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps =
     1.9    let
    1.10      val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
    1.11      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);