diff -r 92e0ed53db25 -r c39994cb152a src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sun May 17 07:17:39 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon May 18 09:48:06 2009 +0200
@@ -45,7 +45,7 @@
      Nitpick_Const_Psimp_Thms.add]
 
 fun note_theorem ((name, atts), ths) =
-  LocalTheory.note Thm.generated_theoremK ((Binding.qualified_name name, atts), ths)
+  LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
@@ -56,7 +56,7 @@
                    |> map (apfst (apfst extra_qualify))
 
       val (saved_spec_simps, lthy) =
-        fold_map (LocalTheory.note Thm.generated_theoremK) spec lthy
+        fold_map (LocalTheory.note Thm.generatedK) spec lthy
 
       val saved_simps = flat (map snd saved_spec_simps)
       val simps_by_f = sort saved_simps