src/HOL/HOL.thy
changeset 28054 2b84d34c5d02
parent 28012 2308843f8b66
child 28227 77221ee0f7b9
     1.1 --- a/src/HOL/HOL.thy	Thu Aug 28 22:08:11 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Aug 28 22:09:20 2008 +0200
     1.3 @@ -29,7 +29,10 @@
     1.4    "~~/src/Tools/code/code_name.ML"
     1.5    "~~/src/Tools/code/code_funcgr.ML"
     1.6    "~~/src/Tools/code/code_thingol.ML"
     1.7 +  "~~/src/Tools/code/code_printer.ML"
     1.8    "~~/src/Tools/code/code_target.ML"
     1.9 +  "~~/src/Tools/code/code_ml.ML"
    1.10 +  "~~/src/Tools/code/code_haskell.ML"
    1.11    "~~/src/Tools/nbe.ML"
    1.12  begin
    1.13  
    1.14 @@ -1703,9 +1706,10 @@
    1.15  hide const eq
    1.16  
    1.17  setup {*
    1.18 -  CodeUnit.add_const_alias @{thm equals_eq}
    1.19 -  #> CodeName.setup
    1.20 -  #> CodeTarget.setup
    1.21 +  Code_Unit.add_const_alias @{thm equals_eq}
    1.22 +  #> Code_Name.setup
    1.23 +  #> Code_ML.setup
    1.24 +  #> Code_Haskell.setup
    1.25    #> Nbe.setup
    1.26  *}
    1.27