--- a/src/HOL/Tools/primrec.ML Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Tools/primrec.ML Wed Oct 21 17:34:35 2009 +0200
@@ -272,7 +272,7 @@
(Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]);
+ [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]);
in
lthy
|> set_group ? LocalTheory.set_group (serial_string ())