fixed codegen setup
authorhaftmann
Thu Aug 16 11:45:06 2007 +0200 (2007-08-16)
changeset 242937e67b9706211
parent 24292 26ac9fe0e80e
child 24294 edfe16773fd4
fixed codegen setup
src/HOL/Code_Setup.thy
src/HOL/HOL.thy
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Code_Setup.thy	Thu Aug 16 11:45:05 2007 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Thu Aug 16 11:45:06 2007 +0200
     1.3 @@ -152,8 +152,6 @@
     1.4  
     1.5  subsection {* Normalization by evaluation *}
     1.6  
     1.7 -setup Nbe.setup
     1.8 -
     1.9  method_setup normalization = {*
    1.10    Method.no_args (Method.SIMPLE_METHOD'
    1.11      (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
     2.1 --- a/src/HOL/HOL.thy	Thu Aug 16 11:45:05 2007 +0200
     2.2 +++ b/src/HOL/HOL.thy	Thu Aug 16 11:45:06 2007 +0200
     2.3 @@ -1652,7 +1652,7 @@
     2.4  
     2.5  subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *}
     2.6  
     2.7 -setup "CodeName.setup #> CodeTarget.setup #> Codegen.setup"
     2.8 +setup "CodeName.setup #> CodeTarget.setup #> Codegen.setup #> Nbe.setup"
     2.9  
    2.10  class eq (attach "op =") = type
    2.11  
     3.1 --- a/src/Pure/codegen.ML	Thu Aug 16 11:45:05 2007 +0200
     3.2 +++ b/src/Pure/codegen.ML	Thu Aug 16 11:45:06 2007 +0200
     3.3 @@ -1024,7 +1024,8 @@
     3.4  
     3.5  fun evaluation_conv ct =
     3.6    let val {thy, t, ...} = rep_cterm ct
     3.7 -  in Thm.invoke_oracle_i thy "Code_Setup.evaluation" (thy, Evaluation t) end;
     3.8 +  in Thm.invoke_oracle_i thy "HOL.evaluation" (thy, Evaluation t) end;
     3.9 +  (*FIXME get rid of hardwired theory name*)
    3.10  
    3.11  
    3.12  (**** Interface ****)