src/HOL/HOL.thy
changeset 29505 c6d2d23909d1
parent 29105 8f38bf68d42e
child 29608 564ea783ace8
     1.1 --- a/src/HOL/HOL.thy	Fri Jan 16 08:28:53 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Jan 16 08:29:11 2009 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4    "~~/src/Tools/code/code_ml.ML"
     1.5    "~~/src/Tools/code/code_haskell.ML"
     1.6    "~~/src/Tools/nbe.ML"
     1.7 -  ("~~/src/HOL/Tools/recfun_codegen.ML")
     1.8 +  ("Tools/recfun_codegen.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Primitive logic *}
    1.12 @@ -1690,7 +1690,7 @@
    1.13  
    1.14  text {* Module setup *}
    1.15  
    1.16 -use "~~/src/HOL/Tools/recfun_codegen.ML"
    1.17 +use "Tools/recfun_codegen.ML"
    1.18  
    1.19  setup {*
    1.20    Code_ML.setup