diff -r 9446cb8e1f65 -r 57b489b54914 src/HOL/blastdata.ML
--- a/src/HOL/blastdata.ML	Fri Dec 30 16:56:57 2005 +0100
+++ b/src/HOL/blastdata.ML	Fri Dec 30 16:56:58 2005 +0100
@@ -16,6 +16,8 @@
 structure Blast_Data = 
   struct
   type claset	= Classical.claset
+  val equality_name = "op ="
+  val not_name = "Not"
   val notE	= notE
   val ccontr	= ccontr
   val contr_tac = Classical.contr_tac