author | wenzelm |
Fri, 24 Jul 2009 22:59:28 +0200 | |
changeset 32182 | f01207d56583 |
parent 32181 | 7e460c2d4223 |
child 32183 | 678f14c9afb5 |
--- 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 ****)