--- a/ProgTutorial/Package/Ind_Extensions.thy	Thu Oct 04 13:00:31 2012 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Sat Dec 01 14:51:19 2012 +0000
@@ -192,7 +192,7 @@
 
 text {* Type declarations *}
 
-ML %grayML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
+ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
 
 ML %grayML{*fun pat_completeness_auto ctxt =