--- a/src/HOL/HOL.thy Tue Sep 08 18:31:26 2009 +0200
+++ b/src/HOL/HOL.thy Wed Sep 09 11:31:20 2009 +0200
@@ -1887,7 +1887,7 @@
*}
setup {*
- Code.add_const_alias @{thm equals_alias_cert}
+ Nbe.add_const_alias @{thm equals_alias_cert}
*}
hide (open) const eq