--- a/src/Tools/nbe.ML Sun Jan 03 15:09:02 2010 +0100
+++ b/src/Tools/nbe.ML Mon Jan 04 14:09:56 2010 +0100
@@ -513,15 +513,14 @@
(* compilation, evaluation and reification *)
-fun compile_eval thy naming program vs_t deps =
+fun compile_eval theory naming program vs_t deps =
let
- val ctxt = ProofContext.init thy;
val (_, (gr, (_, idx_tab))) =
- Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
+ Nbe_Functions.change theory (fn thy => ensure_stmts (ProofContext.init thy) naming program o snd);
in
vs_t
- |> eval_term ctxt gr deps
- |> term_of_univ thy program idx_tab
+ |> eval_term (ProofContext.init theory) gr deps
+ |> term_of_univ theory program idx_tab
end;
(* evaluation with type reconstruction *)