diff -r b6fc4d1b75d0 -r 21b5d0145fe4 ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Tue May 17 19:25:33 2011 +0200
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Tue May 17 19:46:53 2011 +0200
@@ -197,7 +197,7 @@
 
 ML{*fun pat_completeness_auto ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1
-    THEN auto_tac (clasimpset_of ctxt)*}
+    THEN auto_tac ctxt*}
 
 ML {*
   val conf = Function_Common.default_config