diff -r f599ac41e7f5 -r 57cd50f98fdc src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Oct 28 17:15:52 2011 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri Oct 28 22:17:30 2011 +0200
@@ -128,7 +128,8 @@
         val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
       in
         (info,
-         lthy |> Local_Theory.declaration false (add_function_data o transform_function_data info))
+         lthy |> Local_Theory.declaration {syntax = false, pervasive = false}
+          (add_function_data o transform_function_data info))
       end
   in
     ((goal_state, afterqed), lthy')
@@ -203,7 +204,8 @@
             in
               (info',
                lthy 
-               |> Local_Theory.declaration false (add_function_data o transform_function_data info')
+               |> Local_Theory.declaration {syntax = false, pervasive = false}
+                 (add_function_data o transform_function_data info')
                |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
             end)
         end