# HG changeset patch
# User wenzelm
# Date 1248469168 -7200
# Node ID f01207d56583be0cb0693709b3b2855ae6fef354
# Parent  7e460c2d4223a05452c62c113340c36c5984711f
eliminated OldGoals.read_term;

diff -r 7e460c2d4223 -r f01207d56583 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Jul 24 22:59:08 2009 +0200
+++ b/src/Pure/codegen.ML	Fri Jul 24 22:59:28 2009 +0200
@@ -831,7 +831,8 @@
   end;
 
 val generate_code_i = gen_generate_code Sign.cert_term;
-val generate_code = gen_generate_code OldGoals.read_term;
+val generate_code =
+  gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init);
 
 
 (**** Reflection ****)