--- a/src/HOL/cladata.ML Tue Jan 16 00:27:37 2001 +0100
+++ b/src/HOL/cladata.ML Tue Jan 16 00:28:50 2001 +0100
@@ -38,6 +38,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
@@ -47,7 +51,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 Classical = ClassicalFun(Classical_Data);