--- a/ProgTutorial/Package/Ind_Extensions.thy	Fri Jun 05 04:17:28 2009 +0200
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Tue Jun 23 04:05:01 2009 +0200
@@ -184,7 +184,7 @@
   The standard inductive package is based on least fix-points. It allows more 
   general introduction rules that can include any monotone operators and also
   provides a richer reasoning infrastructure. The code of this package can be found in 
-  @{ML_file "HOL/Tools/inductive_package.ML"}.
+  @{ML_file "HOL/Tools/inductive.ML"}.
   \end{readmore}
 *}
 
@@ -192,7 +192,7 @@
 
 text {* Type declarations *}
 
-ML{*TypedefPackage.add_typedef false NONE (@{binding test},[],NoSyn)
+ML{*Typedef.add_typedef false NONE (@{binding test},[],NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}