--- a/ProgTutorial/Package/Ind_Extensions.thy	Mon Apr 26 05:20:01 2010 +0200
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Mon May 17 17:27:21 2010 +0100
@@ -195,5 +195,22 @@
 ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
 
+ML{*fun pat_completeness_auto ctxt =
+  Pat_Completeness.pat_completeness_tac ctxt 1
+    THEN auto_tac (clasimpset_of ctxt)*}
+
+ML {*
+  val conf = Function_Common.default_config
+*}
+
+datatype foo = Foo nat
+
+local_setup{*Primrec.add_primrec [(@{binding "bar"}, NONE, NoSyn)] 
+    [(Attrib.empty_binding, @{term "\<And>x. bar (Foo x) = x"})]
+  #> snd *}
+
+local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] 
+    [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})]
+      conf pat_completeness_auto #> snd*}
 
 (*<*)end(*>*)
\ No newline at end of file