--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Wed Dec 28 17:22:16 2016 +0100
@@ -261,7 +261,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 (fn eq => ((Binding.empty_atts, eq), [], [])) eqs)
+ |> primrec false [] [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs)
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;