--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Aug 19 11:56:12 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Tue Aug 23 15:19:32 2016 +0200
@@ -535,9 +535,9 @@
fun old_of_new f (ts, _, simpss) = (ts, f simpss);
-val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec;
-val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global;
-val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded;
+val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec [];
+val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global [];
+val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded [];
val primrec_simple = apfst (apfst fst o apsnd (old_of_new (flat o snd))) ooo
BNF_LFP_Rec_Sugar.primrec_simple;