# HG changeset patch
# User haftmann
# Date 1187257506 -7200
# Node ID 7e67b9706211d3890a8b4f4bf48f3342a85e1409
# Parent  26ac9fe0e80ead36aa9fa7b1ef5595c84b230cde
fixed codegen setup

diff -r 26ac9fe0e80e -r 7e67b9706211 src/HOL/Code_Setup.thy
--- 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)
diff -r 26ac9fe0e80e -r 7e67b9706211 src/HOL/HOL.thy
--- 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
 
diff -r 26ac9fe0e80e -r 7e67b9706211 src/Pure/codegen.ML
--- 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 ****)