src/Provers/clasimp.ML

   structure Blast: BLAST
   sharing type Classical.claset = Blast.claset
   val notE: thm
   val iffD1: thm
   val iffD2: thm
-  val cla_make_elim: thm -> thm
 end
 
 signature CLASIMP =
 sig
   include CLASIMP_DATA

     val n = nprems_of th;
     val (elim, intro) = if n = 0 then decls1 else decls2;
     val zero_rotate = zero_var_indexes o rotate_prems n;
   in
     (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
-           [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
+           [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))])
       handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
         handle THM _ => intro (cs, [th])),
      simp (ss, [th]))
   end;
 
 fun delIff delcs delss ((cs, ss), th) =
   let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
     (delcs (cs, [zero_rotate (th RS Data.iffD2),
-        Data.cla_make_elim (zero_rotate (th RS Data.iffD1))])
+        Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
       handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
         handle THM _ => delcs (cs, [th])),
      delss (ss, [th]))
   end;