--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Apr 28 09:43:11 2016 +0200
@@ -265,7 +265,7 @@
val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
|> Local_Theory.open_target |> snd
|> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
- |> primrec [(b, NONE, NoSyn)] (map (pair Attrib.empty_binding) eqs)
+ |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [])) eqs)
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;