src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/FOL.thy	Mon Dec 20 16:44:33 2010 +0100
@@ -175,7 +175,7 @@
   (
     val thy = @{theory}
     type claset = Cla.claset
-    val equality_name = @{const_name "op ="}
+    val equality_name = @{const_name eq}
     val not_name = @{const_name Not}
     val notE = @{thm notE}
     val ccontr = @{thm ccontr}
@@ -391,4 +391,7 @@
 setup Induct.setup
 declare case_split [cases type: o]
 
+
+hide_const (open) eq
+
 end