changeset 29505 | c6d2d23909d1 |
parent 29105 | 8f38bf68d42e |
child 29608 | 564ea783ace8 |
--- a/src/HOL/HOL.thy Fri Jan 16 08:28:53 2009 +0100 +++ b/src/HOL/HOL.thy Fri Jan 16 08:29:11 2009 +0100 @@ -35,7 +35,7 @@ "~~/src/Tools/code/code_ml.ML" "~~/src/Tools/code/code_haskell.ML" "~~/src/Tools/nbe.ML" - ("~~/src/HOL/Tools/recfun_codegen.ML") + ("Tools/recfun_codegen.ML") begin subsection {* Primitive logic *} @@ -1690,7 +1690,7 @@ text {* Module setup *} -use "~~/src/HOL/Tools/recfun_codegen.ML" +use "Tools/recfun_codegen.ML" setup {* Code_ML.setup