diff -r de49d5780f57 -r 74f0a06f751f ProgTutorial/Package/Simple_Inductive_Package.thy --- a/ProgTutorial/Package/Simple_Inductive_Package.thy Thu Aug 20 14:19:39 2009 +0200 +++ b/ProgTutorial/Package/Simple_Inductive_Package.thy Thu Aug 20 22:30:20 2009 +0200 @@ -54,7 +54,7 @@ thm rel.accpart'.induct *) -use_chunks "simple_inductive_package.ML" +use "simple_inductive_package.ML" end