eliminated OldGoals.read_term;
authorwenzelm
Fri, 24 Jul 2009 22:59:28 +0200
changeset 32182 f01207d56583
parent 32181 7e460c2d4223
child 32183 678f14c9afb5
eliminated OldGoals.read_term;
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 ****)