src/HOL/HOL.thy
changeset 32544 e129333b9df0
parent 32402 5731300da417
child 32660 e3aab585531d
     1.1 --- a/src/HOL/HOL.thy	Tue Sep 08 18:31:26 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Sep 09 11:31:20 2009 +0200
     1.3 @@ -1887,7 +1887,7 @@
     1.4  *}
     1.5  
     1.6  setup {*
     1.7 -  Code.add_const_alias @{thm equals_alias_cert}
     1.8 +  Nbe.add_const_alias @{thm equals_alias_cert}
     1.9  *}
    1.10  
    1.11  hide (open) const eq