--- a/ProgTutorial/Package/Ind_Extensions.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -193,7 +193,7 @@
 text {* Type declarations *}
 
 ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn)
-  @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
+  @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *}
 
 ML %grayML{*fun pat_completeness_auto ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1