src/HOL/Tools/function_package/size.ML
changeset 29866 6e93ae65c678
parent 29863 dadad1831e9d
child 30190 479806475f3c
--- a/src/HOL/Tools/function_package/size.ML	Fri Feb 06 16:00:05 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Mon Feb 09 10:37:59 2009 +0100
@@ -209,7 +209,7 @@
 
     val ([size_thms], thy'') =  PureThy.add_thmss
       [((Binding.name "size", size_eqns),
-        [Simplifier.simp_add, Nitpick_Const_Simps_Thms.add,
+        [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
          Thm.declaration_attribute
              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
 
@@ -239,4 +239,4 @@
 
 val setup = DatatypePackage.interpretation add_size_thms;
 
-end;
\ No newline at end of file
+end;