--- a/src/FOL/FOL.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/FOL/FOL.thy Sat Oct 17 14:43:18 2009 +0200
@@ -174,13 +174,13 @@
structure Blast = Blast
(
val thy = @{theory}
- type claset = Cla.claset
+ type claset = Cla.claset
val equality_name = @{const_name "op ="}
val not_name = @{const_name Not}
- val notE = @{thm notE}
- val ccontr = @{thm ccontr}
+ val notE = @{thm notE}
+ val ccontr = @{thm ccontr}
val contr_tac = Cla.contr_tac
- val dup_intr = Cla.dup_intr
+ val dup_intr = Cla.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
val rep_cs = Cla.rep_cs
val cla_modifiers = Cla.cla_modifiers