--- a/ProgTutorial/Package/Ind_Extensions.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Tue May 14 11:10:53 2019 +0200
@@ -208,7 +208,7 @@
 datatype foo = Foo nat
 
 local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] 
-    [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})]
+    [((Binding.empty_atts,@{term "\<And>x. baz (Foo x) = x"}),[],[])]
       conf pat_completeness_auto #> snd*}
 
 (*<*)end(*>*)