changeset 32182 | f01207d56583 |
parent 32085 | 26512612005b |
child 32738 | 15bb09ca0378 |
--- 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 ****)