--- a/src/HOL/Tools/code_evaluation.ML Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Sat Apr 16 16:15:37 2011 +0200
@@ -223,6 +223,6 @@
#> Code.datatype_interpretation ensure_term_of_code
#> Code.abstype_interpretation ensure_abs_term_of_code
#> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
- #> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of);
+ #> Value.add_evaluator ("code", dynamic_value_strict o Proof_Context.theory_of);
end;