--- a/src/FOL/cladata.ML Sun Oct 14 19:59:15 2001 +0200
+++ b/src/FOL/cladata.ML Sun Oct 14 19:59:55 2001 +0200
@@ -15,10 +15,6 @@
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
@@ -28,7 +24,6 @@
val classical = classical
val sizef = size_of_thm
val hyp_subst_tacs=[hyp_subst_tac]
- val atomize = atomize_rules
end;
structure Cla = ClassicalFun(Classical_Data);