changeset 36610 | bafd82950e24 |
parent 35845 | e5980f0ad025 |
child 36615 | 88756a5a92fc |
--- a/src/Tools/nbe.ML Mon May 03 07:59:51 2010 +0200 +++ b/src/Tools/nbe.ML Mon May 03 14:25:56 2010 +0200 @@ -521,7 +521,7 @@ fun compile_eval thy program vs_t deps = let - val ctxt = ProofContext.init thy; + val ctxt = ProofContext.init_global thy; val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts ctxt program); in