--- 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