--- a/ProgTutorial/Base.thy	Mon Sep 17 00:07:40 2012 +0100
+++ b/ProgTutorial/Base.thy	Thu Oct 04 13:00:31 2012 +0100
@@ -5,9 +5,6 @@
          "ML_prf" :: prf_decl and
          "ML_val" :: diag
 *)
-uses
-  ("output_tutorial.ML")
-  ("antiquote_setup.ML")
 begin
 
 notation (latex output)
@@ -27,8 +24,8 @@
   HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
 *}
 
-use "output_tutorial.ML"
-use "antiquote_setup.ML"
+ML_file "output_tutorial.ML"
+ML_file "antiquote_setup.ML"
 
 setup {* OutputTutorial.setup *}
 setup {* AntiquoteSetup.setup *}