--- a/Nominal/nominal_termination.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_termination.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -71,7 +71,8 @@
             in
               (info',
                lthy 
-               |> Local_Theory.declaration false (add_function_data o morph_function_data info')
+               |> Local_Theory.declaration {syntax = false, pervasive = false}
+                    (add_function_data o morph_function_data info')
                |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
             end)
         end