| changeset 24293 | 7e67b9706211 |
| parent 24280 | c9867bdf2424 |
| child 24456 | 8eb0f4a36d04 |
--- a/src/Pure/codegen.ML Thu Aug 16 11:45:05 2007 +0200 +++ b/src/Pure/codegen.ML Thu Aug 16 11:45:06 2007 +0200 @@ -1024,7 +1024,8 @@ fun evaluation_conv ct = let val {thy, t, ...} = rep_cterm ct - in Thm.invoke_oracle_i thy "Code_Setup.evaluation" (thy, Evaluation t) end; + in Thm.invoke_oracle_i thy "HOL.evaluation" (thy, Evaluation t) end; + (*FIXME get rid of hardwired theory name*) (**** Interface ****)