--- a/src/HOL/Code_Setup.thy Thu Aug 16 11:45:05 2007 +0200
+++ b/src/HOL/Code_Setup.thy Thu Aug 16 11:45:06 2007 +0200
@@ -152,8 +152,6 @@
subsection {* Normalization by evaluation *}
-setup Nbe.setup
-
method_setup normalization = {*
Method.no_args (Method.SIMPLE_METHOD'
(CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
--- a/src/HOL/HOL.thy Thu Aug 16 11:45:05 2007 +0200
+++ b/src/HOL/HOL.thy Thu Aug 16 11:45:06 2007 +0200
@@ -1652,7 +1652,7 @@
subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *}
-setup "CodeName.setup #> CodeTarget.setup #> Codegen.setup"
+setup "CodeName.setup #> CodeTarget.setup #> Codegen.setup #> Nbe.setup"
class eq (attach "op =") = type
--- 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 ****)