Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/size.ML
changeset 31902 862ae16a799d
parent 31784 bd3486c57ba3
child 32712 ec5976f4d3d8 
--- a/src/HOL/Tools/Function/size.ML	Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML	Thu Jul 02 17:34:14 2009 +0200
@@ -209,7 +209,7 @@
 
     val ([size_thms], thy'') =  PureThy.add_thmss
       [((Binding.name "size", size_eqns),
-        [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+        [Simplifier.simp_add, Nitpick_Const_Simps.add,
          Thm.declaration_attribute
              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
isabelle