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_package/fundef_package.ML
changeset 29863 dadad1831e9d
parent 29581 b3b33e0298eb
child 29866 6e93ae65c678 
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Feb 06 13:43:19 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Feb 06 15:57:47 2009 +0100
@@ -42,7 +42,8 @@
 
 fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
     let
-      val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
+      val atts = Attrib.internal (K Simplifier.simp_add) ::
+                 Attrib.internal (K Nitpick_Const_Simps_Thms.add) :: moreatts
       val spec = post simps
                    |> map (apfst (apsnd (append atts)))
                    |> map (apfst (apfst extra_qualify))
isabelle