# HG changeset patch
# User haftmann
# Date 1207309221 -7200
# Node ID 046e63c9165ccce828eb9327b5d73b1399861c71
# Parent  5ee45391576e0b968423446ef29a5726e1cf53c3
postprocessing of equality

diff -r 5ee45391576e -r 046e63c9165c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Apr 03 23:55:11 2008 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 04 13:40:21 2008 +0200
@@ -1673,10 +1673,13 @@
 lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
 
+declare equals_eq [symmetric, code post]
+
 end
 
 setup {*
-  CodeUnit.add_const_alias @{thm equals_eq}
+  Sign.hide_names_i true ("const", ["HOL.eq"])
+  #> CodeUnit.add_const_alias @{thm equals_eq}
 *}
 
 lemma [code func]:
diff -r 5ee45391576e -r 046e63c9165c src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Thu Apr 03 23:55:11 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy	Fri Apr 04 13:40:21 2008 +0200
@@ -8,8 +8,6 @@
 imports Main "~~/src/HOL/Real/Rational"
 begin
 
-declare equals_eq [symmetric, code post]
-
 lemma "True" by normalization
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code func]