--- a/src/HOL/Nominal/nominal_atoms.ML Mon May 30 11:44:41 2016 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon May 30 14:15:44 2016 +0200
@@ -192,7 +192,7 @@
thy' |>
BNF_LFP_Compat.primrec_global
[(Binding.name swap_name, SOME swapT, NoSyn)]
- [((Attrib.empty_binding, def1), [])] ||>
+ [((Attrib.empty_binding, def1), [], [])] ||>
Sign.parent_path ||>>
Global_Theory.add_defs_unchecked true
[((Binding.name name, def2), [])] |>> (snd o fst)
@@ -226,7 +226,7 @@
thy' |>
BNF_LFP_Compat.primrec_global
[(Binding.name prm_name, SOME prmT, NoSyn)]
- (map (fn def => ((Attrib.empty_binding, def), [])) [def1, def2]) ||>
+ (map (fn def => ((Attrib.empty_binding, def), [], [])) [def1, def2]) ||>
Sign.parent_path
end) ak_names_types thy3;