# HG changeset patch
# User haftmann
# Date 1282633577 -7200
# Node ID 975e4f729127b9585c0cf40180ade4bdadac8a52
# Parent  1c483d137371fd13985d33c46073595c189e9fa3
tuned

diff -r 1c483d137371 -r 975e4f729127 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon Aug 23 11:57:32 2010 +0200
+++ b/src/Tools/nbe.ML	Tue Aug 24 09:06:17 2010 +0200
@@ -530,12 +530,12 @@
 
 (* compilation, evaluation and reification *)
 
-fun compile_eval thy program vs_t deps =
+fun compile_eval thy program =
   let
     val ctxt = ProofContext.init_global thy;
     val (gr, (_, idx_tab)) =
       Nbe_Functions.change thy (ensure_stmts ctxt program);
-  in
+  in fn vs_t => fn deps =>
     vs_t
     |> eval_term ctxt gr deps
     |> term_of_univ thy program idx_tab
@@ -587,7 +587,7 @@
     t
     |> fold_rev lambda frees
     |> rew
-    |> (fn t' => Term.betapplys (t', frees))
+    |> curry (Term.betapplys o swap) frees
   end;
 
 val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy