diff -r e23abeef8150 -r de95ba2760fe src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Tue Jan 16 00:27:37 2001 +0100
+++ b/src/FOL/cladata.ML	Tue Jan 16 00:28:50 2001 +0100
@@ -15,6 +15,10 @@
   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
@@ -24,7 +28,7 @@
   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 Cla = ClassicalFun(Classical_Data);