--- a/src/HOL/Tools/function_package/size.ML Fri Feb 06 13:43:19 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Fri Feb 06 15:57:47 2009 +0100
@@ -209,8 +209,9 @@
val ([size_thms], thy'') = PureThy.add_thmss
[((Binding.name "size", size_eqns),
- [Simplifier.simp_add, Thm.declaration_attribute
- (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
+ [Simplifier.simp_add, Nitpick_Const_Simps_Thms.add,
+ Thm.declaration_attribute
+ (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
in
SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))