diff -r 944b19ab6003 -r 121aa59b4d17 src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Fri May 27 10:30:08 2011 +0200 +++ b/src/Tools/Code_Generator.thy Fri May 27 10:30:08 2011 +0200 @@ -8,7 +8,7 @@ imports Pure uses "~~/src/Tools/cache_io.ML" - "~~/src/Tools/auto_tools.ML" + "~~/src/Tools/try.ML" "~~/src/Tools/solve_direct.ML" "~~/src/Tools/quickcheck.ML" "~~/src/Tools/value.ML"