src/FOL/FOL.thy

 ML {*
   structure Blast = Blast
   (
     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}
     val contr_tac = Cla.contr_tac
     val dup_intr = Cla.dup_intr

 *}
 
 setup Induct.setup
 declare case_split [cases type: o]
 
+
+hide_const (open) eq
+
 end