--- a/ProgTutorial/Package/Simple_Inductive_Package.thy	Mon Sep 17 00:07:40 2012 +0100
+++ b/ProgTutorial/Package/Simple_Inductive_Package.thy	Thu Oct 04 13:00:31 2012 +0100
@@ -1,9 +1,10 @@
 theory Simple_Inductive_Package
 imports Main "../Base"
 keywords "simple_inductive" :: thy_decl
-uses "simple_inductive_package.ML"
 begin
 
+ML_file "simple_inductive_package.ML"
+
 (*
 simple_inductive
   trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"