ProgTutorial/Package/Ind_Extensions.thy
changeset 464 21b5d0145fe4
parent 423 0a25b35178c3
child 517 d8c376662bb4
--- 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