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/Nominal/nominal_primrec.ML
changeset 31902 862ae16a799d
parent 31723 f5cafe803b55
child 31938 f193d95b4632 
--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Jul 02 17:34:14 2009 +0200
@@ -373,7 +373,7 @@
            lthy''
            |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
                 map (Attrib.internal o K)
-                    [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
+                    [Simplifier.simp_add, Nitpick_Const_Simps.add]),
                 maps snd simps')
            |> snd
          end)
isabelle