--- a/ProgTutorial/Package/Ind_Extensions.thy	Fri May 17 11:01:55 2013 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Tue May 28 23:26:18 2013 +0100
@@ -192,8 +192,10 @@
 
 text {* Type declarations *}
 
+(*
 ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *}
+*)
 
 ML %grayML{*fun pat_completeness_auto ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1