src/HOL/blastdata.ML
changeset 18171 c4f873d65603
parent 16774 515b6020cf5d
child 18524 57b489b54914
--- a/src/HOL/blastdata.ML	Mon Nov 14 16:26:40 2005 +0100
+++ b/src/HOL/blastdata.ML	Mon Nov 14 18:25:34 2005 +0100
@@ -16,7 +16,6 @@
 structure Blast_Data = 
   struct
   type claset	= Classical.claset
-  val is_hol    = true
   val notE	= notE
   val ccontr	= ccontr
   val contr_tac = Classical.contr_tac