1.1 --- a/src/Tools/nbe.ML	Mon Aug 23 11:57:32 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Aug 24 09:06:17 2010 +0200
     1.3 @@ -530,12 +530,12 @@
     1.4  
     1.5  (* compilation, evaluation and reification *)
     1.6  
     1.7 -fun compile_eval thy program vs_t deps =
     1.8 +fun compile_eval thy program =
     1.9    let
    1.10      val ctxt = ProofContext.init_global thy;
    1.11      val (gr, (_, idx_tab)) =
    1.12        Nbe_Functions.change thy (ensure_stmts ctxt program);
    1.13 -  in
    1.14 +  in fn vs_t => fn deps =>
    1.15      vs_t
    1.16      |> eval_term ctxt gr deps
    1.17      |> term_of_univ thy program idx_tab
    1.18 @@ -587,7 +587,7 @@
    1.19      t
    1.20      |> fold_rev lambda frees
    1.21      |> rew
    1.22 -    |> (fn t' => Term.betapplys (t', frees))
    1.23 +    |> curry (Term.betapplys o swap) frees
    1.24    end;
    1.25  
    1.26  val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy