src/HOL/HOL.thy

 apply (tactic {* etac (Classical.dup_elim @{thm allE}) 1 *})
 apply iprover
 done
 
 ML {*
-structure Blast = BlastFun
+structure Blast = Blast
 (
+  val thy = @{theory}
   type claset = Classical.claset
   val equality_name = @{const_name "op ="}
   val not_name = @{const_name Not}
   val notE = @{thm notE}
   val ccontr = @{thm ccontr}