diff -r 308ba2488d40 -r e9fd5eff62c1 ProgTutorial/Recipes/Oracle.thy
--- a/ProgTutorial/Recipes/Oracle.thy	Mon Sep 17 00:07:40 2012 +0100
+++ b/ProgTutorial/Recipes/Oracle.thy	Thu Oct 04 13:00:31 2012 +0100
@@ -1,6 +1,5 @@
 theory Oracle
 imports "../Appendix"
-uses ("external_solver.ML")
 begin
 
 section {* Writing an Oracle (TBD)\label{rec:oracle} *} 
@@ -32,7 +31,7 @@
   ``external solver'':
 *}
 
-use "external_solver.ML"
+ML_file "external_solver.ML"
 
 text {*
   We do, however, know that the solver provides a function