--- a/ProgTutorial/Package/Ind_Extensions.thy Wed Oct 15 23:12:54 2014 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy Wed Oct 15 23:40:05 2014 +0100
@@ -207,10 +207,6 @@
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*}