src/HOL/cladata.ML

 
 (*we don't redeclare the original make_elim (Tactic.make_elim) for 
   compatibliity with strange things done in many existing proofs *)
 val cla_make_elim = Make_Elim.make_elim;
 
+val atomize_rules = thms "atomize'";
+val atomize_tac = Method.atomize_tac atomize_rules;
+val atomize_strip_tac = Method.atomize_strip_tac (atomize_rules, [impI, allI]);
+
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
   struct
   val make_elim = cla_make_elim
   val mp        = mp
   val not_elim  = notE
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  val atomize	= thms "atomize'"
+  val atomize	= atomize_rules
   end;
 
 structure Classical = ClassicalFun(Classical_Data);
 
 structure BasicClassical: BASIC_CLASSICAL = Classical;