diff -r 1d1e4cda8c54 -r 2e199c5faf76 ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Sun Mar 07 21:15:05 2010 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Wed Apr 07 11:12:12 2010 +0200
@@ -192,7 +192,7 @@
 
 text {* Type declarations *}
 
-ML{*Typedef.add_typedef false NONE (@{binding test},[],NoSyn)
+ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}