--- a/src/Pure/codegen.ML Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/codegen.ML Mon May 03 14:25:56 2010 +0200
@@ -822,7 +822,7 @@
val generate_code_i = gen_generate_code Sign.cert_term;
val generate_code =
- gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init);
+ gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init_global);
(**** Reflection ****)
@@ -908,7 +908,7 @@
fun eval_term thy t =
let
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
val e =
let
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse